From f0a784052b42a46827f0c1d89046d2c5b5f2c7d1 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 8 Feb 2012 18:14:23 +0000
Subject: Tweak output strings and prompt matching
---
hol-light/hol-light.el | 4 ++--
hol-light/pg_tactics.ml | 7 ++++---
2 files changed, 6 insertions(+), 5 deletions(-)
(limited to 'hol-light')
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 18192ed1..a0afba1a 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -95,11 +95,11 @@ You need to restart Emacs if you change this setting."
"Value for `proof-shell-interrupt-regexp' with custom top level.")
(defconst hol-light-plain-prompt-regexp
- "^# "
+ "\\(val it : unit = ()\n\\)?^# "
"Value for `proof-shell-annotated-prompt-regexp' with standard top level.")
(defconst hol-light-annotated-prompt-regexp
- ".*"
+ "\\(val it : unit = ()\n\\)?.*"
"Value for `proof-shell-annotated-prompt-regexp' with custom top level.")
(defconst hol-light-plain-error-regexp
diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml
index de6132a9..2943f461 100644
--- a/hol-light/pg_tactics.ml
+++ b/hol-light/pg_tactics.ml
@@ -314,12 +314,13 @@ let pg_kill() =
let n = length (!the_current_xgoalstack) in
(dec_pg_global_state n;
the_current_xgoalstack := [];
- print_string "*** Proof aborted.");;
+ print_string "*** Proof aborted.\n");;
-let pg_forget s = ();; (* TODO *)
+let pg_forget s =
+ print_string ("*** Remove theorem "^s^"\n");;
let pg_restart() =
- print_string "*** Session restarted.";;
+ print_string "*** Session restarted.\n";;
(* ------------------------------------------------------------------------- *)
(* Configure the annotated prompt. *)
--
cgit v1.2.3