Add proof-forget-id command and make top_thm discard the goalstack.

2 files changed, 37 insertions, 16 deletions

diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 05f1ab98..48b6d971 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -52,10 +52,11 @@ You need to restart Emacs if you change this setting."
    (if hol-light-use-custom-toplevel
        (list (format "#use \"%shol-light/pg_tactics.ml\""
 		     proof-home-directory))
-     (list
-      "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;"
-      "let pg_undo n = (pg_repeat n (fun ()->let _ = b() in ()); p());;"
-      "let pg_kill () = current_goalstack:=[];;")))
+  (list
+  "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;"
+  "let pg_undo n = (pg_repeat n (fun ()->let _ = b() in ()); p());;"
+  "let pg_kill () = current_goalstack:=[];;"
+  "let pg_forget id = ();;")))
   "*Commands used to start up a running HOL Light session."
   :type '(list string)
   :group 'hol-light)
@@ -164,6 +165,7 @@ You need to restart Emacs if you change this setting."
  proof-save-command            	"val %s = top_thm();;"
  proof-kill-goal-command       	"pg_kill();;"
  proof-undo-n-times-cmd        	"pg_undo %s;;"
+ proof-forget-id-command	"pg_forget \"%s\";;"
  proof-showproof-command       	"p()"
  proof-auto-multiple-files     	t
  proof-shell-cd-cmd            	"#cd \"%s\";;"
@@ -206,8 +208,6 @@ You need to restart Emacs if you change this setting."
  ;; proof-shell-eager-annotation-start
  proof-find-theorems-command	"DB.match [] (%s);;"
 
- proof-forget-id-command	"();;" ;; candidate for making nil, change generic
-
  ;;
  ;; Syntax and syntax table entries for proof scripts
  ;;
diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml
index 6cbf6784..d0e4f2ce 100644
--- a/hol-light/pg_tactics.ml
+++ b/hol-light/pg_tactics.ml
@@ -225,7 +225,14 @@ let the_current_xgoalstack = ref ([] : goalstack);;
 let pg_proof_state () = length !the_current_xgoalstack;;
 
 (* ------------------------------------------------------------------------- *)
-(* Subgoal package but for xgoals.  These overwrite the existing commands.   *)
+(* Subgoal package for xgoals and with a constrained undo protocol for       *)
+(* interacting with Proof General to track the state.  These overwrite the   *)
+(* existing commands and may cause breakage of interactive proofs.           *)
+(*								             *)
+(* The restrictions are:						     *)
+(*  - top_thm may only be called once and closes the currently open proof.   *)
+(*  - the back command b() is not allowed to appear in a file.		     *)
+(*								             *)
 (* ------------------------------------------------------------------------- *)
 
 let (xrefine:xrefinement->goalstack) =
@@ -270,6 +277,28 @@ let p() = !the_current_xgoalstack;;
 let b() =
   failwith "Undo with b() is not available in Proof General top level";;
 
+let top_realgoal() =
+  let (_,(((asl,w),id)::_),_)::_ = !the_current_xgoalstack in
+  asl,w;;
+
+let top_goal() =
+  let asl,w = top_realgoal() in
+  map (concl o snd) asl,w;;
+
+let plain_top_thm() =
+  let (_,[],f)::_ = !the_current_xgoalstack in
+   f null_inst [];;
+
+let top_thm() = 
+  let t = plain_top_thm() in
+  (inc_pg_global_state();
+   the_current_xgoalstack := [];
+   t);;
+
+(* ------------------------------------------------------------------------- *)
+(* Undo handling functions for Proof General		                     *)
+(* ------------------------------------------------------------------------- *)
+
 let pg_undo n =
   let l = !the_current_xgoalstack in
    if length l < n then failwith "pg_undo: called with too many steps"
@@ -283,17 +312,9 @@ let pg_kill () =
    the_current_xgoalstack := [];
    p());;
 
-let top_realgoal() =
-  let (_,(((asl,w),id)::_),_)::_ = !the_current_xgoalstack in
-  asl,w;;
+let pg_forget s = ();;
 
-let top_goal() =
-  let asl,w = top_realgoal() in
-  map (concl o snd) asl,w;;
 
-let top_thm() =
-  let (_,[],f)::_ = !the_current_xgoalstack in
-  f null_inst [];;
 
 (* ------------------------------------------------------------------------- *)
 (* Configure the annotated prompt.				             *)