Improve handling of undo, implementing pg_kill and pg_undo.

2 files changed, 33 insertions, 33 deletions

diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index f773eb6e..05f1ab98 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -51,14 +51,15 @@ You need to restart Emacs if you change this setting."
 	 "#use \"hol.ml\"")
    (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));;"))
+		     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:=[];;")))
   "*Commands used to start up a running HOL Light session."
   :type '(list string)
   :group 'hol-light)
 
-
 ;;
 ;; Regular expressions for matching output with  
 ;; standard or custom top levels
@@ -161,9 +162,9 @@ You need to restart Emacs if you change this setting."
  proof-non-undoables-regexp    	"b()" ; and others..
  proof-goal-command            	"g `%s`;;"
  proof-save-command            	"val %s = top_thm();;"
- proof-kill-goal-command       	"current_goalstack:=[];;" ; for cleanliness
+ proof-kill-goal-command       	"pg_kill();;"
+ proof-undo-n-times-cmd        	"pg_undo %s;;"
  proof-showproof-command       	"p()"
- proof-undo-n-times-cmd        	"(pg_repeat b %s; p());;"
  proof-auto-multiple-files     	t
  proof-shell-cd-cmd            	"#cd \"%s\";;"
  proof-shell-filename-escapes  	'(("\\\\" . "\\\\") ("\""   . "\\\""))
diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml
index c96c5cdc..6cbf6784 100644
--- a/hol-light/pg_tactics.ml
+++ b/hol-light/pg_tactics.ml
@@ -203,18 +203,18 @@ let (mk_xgoalstate:goal->xgoalstate) =
     else failwith "mk_goalstate: Non-boolean goal";;
 
 (* ------------------------------------------------------------------------- *)
-(* The global state counts the total number of undoable proof steps.         *)
+(* The global state counts the total number of proof steps taken.            *)
 (* ------------------------------------------------------------------------- *)
 
-let the_pt_global_state = ref 1;;
+let the_pg_global_state = ref 1;;
 
-let inc_pt_global_state () =
-  (the_pt_global_state := !the_pt_global_state + 1);;
+let inc_pg_global_state () =
+  (the_pg_global_state := !the_pg_global_state + 1);;
 
-let dec_pt_global_state () =
-  (the_pt_global_state := !the_pt_global_state - 1);;
+let dec_pg_global_state n =
+  (the_pg_global_state := !the_pg_global_state - n);;
 
-let pt_global_state () = !the_pt_global_state;;
+let pg_global_state () = !the_pg_global_state;;
 
 (* ------------------------------------------------------------------------- *)
 (* The proof state number is the length of the current goal stack.           *)
@@ -222,15 +222,7 @@ let pt_global_state () = !the_pt_global_state;;
 
 let the_current_xgoalstack = ref ([] : goalstack);;
 
-let pt_proof_state () = length !the_current_xgoalstack;;
-
-let pt_back_to_proof_state n : goalstack =
-  let pst = pt_proof_state () in
-  if (0 <= n) & (n <= pst)
-    then (the_current_xgoalstack :=
-               snd (chop_list (pst-n) !the_current_xgoalstack);
-          !the_current_xgoalstack)
-    else failwith "Not a valid Prooftree state number";;
+let pg_proof_state () = length !the_current_xgoalstack;;
 
 (* ------------------------------------------------------------------------- *)
 (* Subgoal package but for xgoals.  These overwrite the existing commands.   *)
@@ -250,17 +242,17 @@ let flush_goalstack() =
 
 let e tac =
   let result = xrefine(xby(VALID tac)) in
-  (inc_pt_global_state ();
+  (inc_pg_global_state ();
    the_tactic_flag := true;
    result);;
 
 let r n =
-  (inc_pt_global_state ();
+  (inc_pg_global_state ();
    xrefine(xrotate n));;
 
 let set_goal(asl,w) =
   let aths = map ASSUME asl in
-  (inc_pt_global_state ();
+  (inc_pg_global_state ();
    the_current_xgoalstack :=
      [mk_xgoalstate(map (fun th -> "",th) aths,w)];
    !the_current_xgoalstack);;
@@ -273,16 +265,23 @@ let g t =
    else ());
   set_goal([],t);;
 
+let p() = !the_current_xgoalstack;;
+
 let b() =
+  failwith "Undo with b() is not available in Proof General top level";;
+
+let pg_undo n =
   let l = !the_current_xgoalstack in
-  (* FIXME: this is wrong wrt "global" state, we might try to keep
-     a stack of proof states to be closer. 
-    if length l = 1 then failwith "Can't back up any more" *)
-  (dec_pt_global_state ();
-   the_current_xgoalstack := if length l > 1 then tl l else l;
-   !the_current_xgoalstack);;
+   if length l < n then failwith "pg_undo: called with too many steps"
+   else (dec_pg_global_state n;
+         the_current_xgoalstack := snd (chop_list n l);
+         p());;
 
-let p() = !the_current_xgoalstack;;
+let pg_kill () = 
+  let n = length (!the_current_xgoalstack) in
+  (dec_pg_global_state n;
+   the_current_xgoalstack := [];
+   p());;
 
 let top_realgoal() =
   let (_,(((asl,w),id)::_),_)::_ = !the_current_xgoalstack in
@@ -302,7 +301,7 @@ let top_thm() =
 
 pg_prompt_info := 
    fun () -> 
-   let pst = pt_proof_state () and gst = pt_global_state () in
+   let pst = pg_proof_state () and gst = pg_global_state () in
    string_of_int gst ^ "|" ^ string_of_int pst;;
 
 (* ------------------------------------------------------------------------- *)