Start support for both plain and custom top levels (work in progress).

3 files changed, 329 insertions, 150 deletions

diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 001779ca..1fdafcde 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -13,36 +13,130 @@
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
 
-(defcustom hol-light-home "/home/da/hol_light"
+(defcustom hol-light-home 
+  (or (getenv "HOLLIGHT_HOME")
+      (concat (getenv "HOME") "/hol_light"))
   "*Directory holding the local installation of HOL Light."
   :type 'string
   :group 'hol-light)
 
+(defcustom hol-light-use-custom-toplevel t
+  "*If non-nil, we use a custom toplevel for Proof General.
+This configures extra annotations inside HOL Light to help
+recognise portions of output from the proof assistant.
+
+If this is incompatible with your usage of HOL Light for
+some reason, you can change this setting to run in a
+degraded (less robust) way which interfaces with the
+standard top level.
+
+You need to restart Emacs if you change this setting.")
+
+(defconst hol-light-pre-sync-cmd
+  (format "#use \"%spg_prompt.ml\";; " proof-home-directory)
+  "Command used to configure prompt annotations for Proof General.")
+
 (defcustom hol-light-startup-cmds 
   (list (format "#cd \"%s\"" hol-light-home)
-	"#use \"hol.ml\""
-	(format "#cd \"%s\"" proof-home-directory)
-	"#use \"pg_tactics.ml\"")
+	"#use \"hol.ml\"")
   "*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
+;;
+
+(defconst hol-light-plain-start-goals-regexp
+  (concat
+  "^\\(val it : x?goalstack = \\)"
+  "\\(?:.+\n\\)*"
+  "\\(?:[0-9]*[0-9] subgoals? ([0-9]+ total)\\|No subgoals\\)")
+  "Value for `proof-shell-start-goals-regexp' with standard top level.")
+
+(defconst hol-light-annotated-start-goals-regexp 
+  hol-light-plain-start-goals-regexp
+  "Value for `proof-shell-start-goals-regexp' with custom top level.")
+
+(defconst hol-light-plain-interrupt-regexp
+  "Interrupted"
+  "Value for `proof-shell-interrupt-regexp' with standard top level.")
+
+(defconst hol-light-annotated-interrupt-regexp
+  hol-light-plain-interrupt-regexp ;; TODO
+  "Value for `proof-shell-interrupt-regexp' with custom top level.")  
+
+(defconst hol-light-plain-prompt-regexp
+  "^# "
+  "Value for `proof-shell-annotated-prompt-regexp' with standard top level.")
+
+(defconst hol-light-annotated-prompt-regexp
+  "<prompt>.+</prompt>"
+  "Value for `proof-shell-annotated-prompt-regexp' with custom top level.")
+
+(defconst hol-light-plain-error-regexp
+  (proof-regexp-alt "Characters [0-9]+-[0-9]+:" 
+		    "Exception: Failure"
+		    "Parse error: "
+		    ;; TODO: more here, file not found, etc.
+		    )
+  "Value for `proof-shell-error-regexp' with standard top level.")
+
+(defconst hol-light-annotated-error-regexp 
+  "<error>.+</error>" ;; FIXME: include new lines
+  "Value for `proof-shell-error-regexp' with custom top level.")
+
+(defconst hol-light-plain-proof-completed-regexp
+   "Initial goal proved"
+   "Value for `proof-shell-proof-completed-regexp' with standard top level.")
+
+(defconst hol-light-annotated-proof-completed-regexp
+  hol-light-plain-proof-completed-regexp ;; TODO
+   "Value for `proof-shell-proof-completed-regexp' with standard top level.")
+
+(defconst hol-light-plain-message-start 
+  nil ;; TODO
+  "Value for `proof-shell-eager-annotation-start' with standard top level.")
+
+(defconst hol-light-annotated-message-start
+  nil ;; TODO
+  "Value for `proof-shell-eager-annotation-start' with custom top level.")
+
+(defconst hol-light-plain-message-end
+  nil ;; TODO
+  "Value for `proof-shell-eager-annotation-start' with standard top level.")
+
+(defconst hol-light-annotated-message-end
+  nil ;; TODO
+  "Value for `proof-shell-eager-annotation-start' with custom top level.")
+  
+
+;;;
+;;; State 
+;;;
+
 (defvar hol-light-keywords nil)
 (defvar hol-light-rules nil)
 (defvar hol-light-tactics nil)
 (defvar hol-light-tacticals nil)
 
+
+;;;
+;;; Main configuration
+;;;
+
 (proof-easy-config  'hol-light "HOL Light"
  proof-assistant-home-page       "https://www.cl.cam.ac.uk/~jrh13/hol-light/"
  proof-prog-name		 "ocaml"
  proof-terminal-string           ";;"
- proof-script-comment-start      "(*"
- proof-script-comment-end        "*)"
+ proof-shell-pre-sync-init-cmd   hol-light-pre-sync-cmd
+ proof-shell-startup-cmds        hol-light-startup-cmds
 
- ;; These are all approximations, of course.
+ ;; Regexps for matching tactic script inputs: all approximations, of course.
  proof-goal-command-regexp     	"^g[ `]"
- proof-save-command-regexp     	"pg_top_thm_and_drop"
+ proof-save-command-regexp     	"top_thm()"
  proof-goal-with-hole-regexp   	"let \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*prove"
  proof-save-with-hole-regexp   	"let \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*top_thm()"
  proof-non-undoables-regexp    	"b()" ; and others..
@@ -50,32 +144,44 @@
  proof-save-command            	"val %s = top_thm();;"
  proof-kill-goal-command       	"current_goalstack:=[];;" ; for cleanliness
  proof-showproof-command       	"p()"
- proof-undo-n-times-cmd        	"(pg_repeat b %s; p());;"
+ proof-undo-n-times-cmd        	"(funpow %s b %s; p());;"
  proof-auto-multiple-files     	t
  proof-shell-cd-cmd            	"#cd \"%s\";;"
  proof-shell-filename-escapes  	'(("\\\\" . "\\\\") ("\""   . "\\\""))
- proof-shell-interrupt-regexp   "Interrupted"
- proof-shell-start-goals-regexp  
-(setq proof-shell-start-goals-regexp  
- (concat
-  "^\\(val it : x?goalstack = \\)"
-  "\\(?:.+\n\\)*"
-  "\\(?:[0-9]*[0-9] subgoals? ([0-9]+ total)\\|No subgoals\\)")
- )
 
- proof-shell-annotated-prompt-regexp "^# "
- proof-shell-error-regexp 
- (proof-regexp-alt "Characters [0-9]+-[0-9]+:" 
-		   "Exception: Failure"
-		   "Parse error: ")
- proof-shell-init-cmd
- (append hol-light-startup-cmds
-	 '("let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1))"
-	   "let pg_top_thm_and_drop () = let t = top_thm() in ((let _ = b() in ()); t)"))
+ proof-shell-annotated-prompt-regexp (if hol-light-use-custom-toplevel
+					 hol-light-annotated-prompt-regexp
+				       hol-light-plain-prompt-regexp)
+
+ proof-shell-interrupt-regexp        (if hol-light-use-custom-toplevel
+					 hol-light-annotated-interrupt-regexp
+				       hol-light-plain-interrupt-regexp)
+
+ proof-shell-start-goals-regexp      (if hol-light-use-custom-toplevel
+					 hol-light-annotated-start-goals-regexp
+				       hol-light-plain-start-goals-regexp)
+
+ proof-shell-error-regexp	     (if hol-light-use-custom-toplevel
+					 hol-light-annotated-error-regexp
+				       hol-light-plain-error-regexp)
 
+ proof-shell-proof-completed-regexp  (if hol-light-use-custom-toplevel
+					 hol-light-annotated-proof-completed-regexp
+				       hol-light-plain-proof-completed-regexp)
+
+ proof-shell-eager-annotation-start  (if hol-light-use-custom-toplevel
+					 hol-light-annotated-message-start
+				       hol-light-plain-message-start)
+
+ proof-shell-eager-annotation-end    (if hol-light-use-custom-toplevel
+					 hol-light-annotated-message-end
+				       hol-light-plain-message-end)
+
+ 
  ;; FIXME: add optional help topic parameter to help command.
  proof-info-command		    "help \"hol\""
- proof-shell-proof-completed-regexp "Initial goal proved"
+ proof-shell-proof-completed-regexp
+
  ;; FIXME: next one needs setting so that "urgent" messages are displayed
  ;; eagerly from HOL.
  ;; proof-shell-eager-annotation-start
@@ -83,13 +189,11 @@
 
  proof-forget-id-command	"();;" ;; candidate for making nil, change generic
 
- ;; We must force this to use ptys since mosml doesn't flush its output
- ;; (on Linux, presumably on Solaris too).
- proof-shell-process-connection-type t
-
  ;;
- ;; Syntax table entries for proof scripts
+ ;; Syntax and syntax table entries for proof scripts
  ;;
+ proof-script-comment-start      "(*"
+ proof-script-comment-end        "*)"
  proof-script-syntax-table-entries
  '(?\` "\""
    ?\$ "."
@@ -221,8 +325,9 @@
  )
 
 
+;;;
 ;;; Prooftree configuration  (experimental, ongoing)
-;;
+;;;
 
 ;; regexps for recognising additional markup in output
 
@@ -333,11 +438,4 @@ The not yet delayed output is in the region
 (add-hook 'proof-tree-urgent-action-hook 'hol-light-proof-tree-get-new-subgoals)
 
 
-
-
-
-
-(warn "Hol Light Proof General is incomplete!  Please help improve it!
-Read the manual, make improvements, upload at http://proofgeneral.inf.ed.ac.uk/trac")
-
 (provide 'hol-light)
diff --git a/hol-light/pg_prompt.ml b/hol-light/pg_prompt.ml
new file mode 100644
index 00000000..f52dc76e
--- /dev/null
+++ b/hol-light/pg_prompt.ml
@@ -0,0 +1,41 @@
+(* ========================================================================= *)
+(* HOL Light tweaks for Proof General.				             *)
+(*                                                                           *)
+(* Mark Adams, David Aspinall.						     *)
+(* LFCS, School of Informatics, University of Edinburgh			     *)
+(*                                                                           *)
+(* (c) Copyright University of Edinburgh and authors, 2012.                  *)
+(*									     *)
+(* This file adjust the OCaml prompt to help Proof General synchronization.  *)
+(* It is loaded before HOL Light.					     *)
+(* ========================================================================= *)
+
+
+(* ------------------------------------------------------------------------- *)
+(* Proof General mode, providing extra annotations in output	             *)
+(* ------------------------------------------------------------------------- *)
+
+let pg_mode = ref (true : bool);;
+
+let pg_mode_on () = (pg_mode := true);;
+let pg_mode_off () = (pg_mode := false);;
+
+let pg_prompt_info = ref (fun () -> "");;
+
+
+(* ------------------------------------------------------------------------- *)
+(* Adjust the OCaml prompt to carry information for Proof General.           *)
+(* ------------------------------------------------------------------------- *)
+
+let original_prompt_fn = !Toploop.read_interactive_input in
+(Toploop.read_interactive_input :=
+   fun prompt buffer len ->
+      let prompt' =
+         if (!pg_mode)
+           then "<prompt>" ^
+		(!pg_prompt_info()) ^
+                "</prompt>"
+           else prompt in
+      original_prompt_fn prompt' buffer len);;
+
+
diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml
index ece7a22a..45e8591e 100644
--- a/hol-light/pg_tactics.ml
+++ b/hol-light/pg_tactics.ml
@@ -1,23 +1,30 @@
-(* 
-   Modified HOL Light goalstack to support Hendrik Tew's Prooftree
-   application via Proof General.
-
-   Mark Adams, David Aspinall
-   January 2012.
-
-   This file contains some functions that are modified from the
-   original HOL Light code, and is therefore subject to the HOL Light
-   copyright, see the file LICENSE-HOL-LIGHT in this directory.
-
-   TODO:
-    1) rebind top-level identifiers for g, e, r, b and add a flag
-       to turn on/off extended behaviour
+(* ========================================================================= *)
+(* HOL Light subgoal package amended for Proof General and Prooftree.        *)
+(*                                                                           *)
+(* Mark Adams, David Aspinall.						     *)
+(* LFCS, School of Informatics, University of Edinburgh			     *)
+(*                                                                           *)
+(* (c) Copyright University of Edinburgh and authors, 2012.                  *)
+(*									     *)
+(* This file contains some functions that are modified from the		     *)
+(* original HOL Light code, and is therefore subject to the HOL Light	     *)
+(* copyright, see the file LICENSE-HOL-LIGHT in this directory.		     *)
+(*									     *)
+(* ========================================================================= *)
+(*									     *)
+(* This file overwrites HOL Light's subgoal package commands with variants   *)
+(* that output additional annotations specifically for Prooftree.  These get *)
+(* intercepted by Proof General, which removes them from the output          *)
+(* displayed to the Proof General user.					     *)
+
+(* TODO: 
+   1. add urgent message annotations for errors and strings output during
+      long-running tactics
+   2. fix on/off: don't turn off prompt annotation, support Prooftree on/off.
 *)
 
-
-
 (* ------------------------------------------------------------------------- *)
-(* Goal counter for providing goad ids.                                      *)
+(* Goal counter for providing goal ids.                                      *)
 (* ------------------------------------------------------------------------- *)
 
 type goal_id = int;;
@@ -27,8 +34,7 @@ let string_of_goal_id id = string_of_int id;;
 let the_goal_counter = ref (0 : goal_id);;
 
 let inc_goal_counter () =
-  (the_goal_counter := !the_goal_counter + 1;
-   !the_goal_counter);;
+  (the_goal_counter := !the_goal_counter + 1);;
 
 let reset_goal_counter () =
   (the_goal_counter := 0;
@@ -49,10 +55,10 @@ let dest_xgoal (gx : xgoal) = gx;;
 type xgoalstate = (term list * instantiation) * xgoal list * justification;;
 
 (* ------------------------------------------------------------------------- *)
-(* A goalstack but for xgoals.                                               *)
+(* A goalstack but for xgoals.  Overwrites original HL datatype.             *)
 (* ------------------------------------------------------------------------- *)
 
-type xgoalstack = xgoalstate list;;
+type goalstack = xgoalstate list;;
 
 (* ------------------------------------------------------------------------- *)
 (* A refinement but for xgoals.                                              *)
@@ -61,7 +67,7 @@ type xgoalstack = xgoalstate list;;
 type xrefinement = xgoalstate -> xgoalstate;;
 
 (* ------------------------------------------------------------------------- *)
-(* Apply instantiation to a goal.                                            *)
+(* Instantiation of xgoals.                                                  *)
 (* ------------------------------------------------------------------------- *)
 
 let (inst_xgoal:instantiation->xgoal->xgoal) =
@@ -69,19 +75,26 @@ let (inst_xgoal:instantiation->xgoal->xgoal) =
     (map (I F_F INSTANTIATE_ALL p) thms,instantiate p w),id;;
 
 (* ------------------------------------------------------------------------- *)
-(* A printer for xgoals etc.                                                 *)
+(* A printer for xgoals and xgoalstacks.                                     *)
 (* ------------------------------------------------------------------------- *)
 
 let the_new_goal_ids = ref ([] : goal_id list);;
 
 let the_tactic_flag = ref false;;
 
+let print_string_seplist sep xs =
+  if (xs = [])
+    then ()
+    else (print_string (hd xs);
+          do_list (fun x -> print_string sep; print_string x) (tl xs));;
+
 let print_xgoal ((g,id) : xgoal) : unit =
-  (print_string ("[Goal ID " ^ string_of_goal_id id ^ "]");
-   print_newline ();
+  ((if (!pg_mode)
+      then (print_string ("[Goal ID " ^ string_of_goal_id id ^ "]");
+            print_newline ()));
    print_goal g);;
 
-let (print_xgoalstack:xgoalstack->unit) =
+let (print_xgoalstack:goalstack->unit) =
   let print_xgoalstate k gs =
     let (_,gl,_) = gs in
     let n = length gl in
@@ -91,35 +104,48 @@ let (print_xgoalstack:xgoalstack->unit) =
     print_string s; print_newline();
     if gl = [] then () else
     (do_list (print_xgoal o C el gl) (rev(1--(k-1)));
-     print_string "[*]";
+     (if (!pg_mode) then print_string "[*]");
      print_xgoal (el 0 gl)) in
   fun l ->
-   (print_string ("[State Counter " ^ string_of_int (length l) ^ "]");
-    (if (!the_tactic_flag)
+   ((if (!pg_mode) & (!the_tactic_flag)
        then let xs = map string_of_int (!the_new_goal_ids) in
-            the_tactic_flag := false;
-            if (length xs > 0) then
-              print_string
-                ("[New Goal IDs: " ^
-                 end_itlist (fun x1 x2 -> x1 ^ " " ^ x2) xs ^ "]"));
-    print_newline ();
-    if l = [] then print_string "Empty goalstack"
-    else if tl l = [] then
-      let (_,gl,_ as gs) = hd l in
-      print_xgoalstate 1 gs
-    else
-      let (_,gl,_ as gs) = hd l
-      and (_,gl0,_) = hd(tl l) in
-      let p = length gl - length gl0 in
-      let p' = if p < 1 then 1 else p + 1 in
-      print_xgoalstate p' gs);;
+            (the_tactic_flag := false;
+             print_string  "[New Goal IDs: ";
+             print_string_seplist " " xs;
+             print_string "]";
+             print_newline ()));
+    (if l = [] then print_string "Empty goalstack"
+     else if tl l = [] then
+       let (_,gl,_ as gs) = hd l in
+       print_xgoalstate 1 gs
+     else
+       let (_,gl,_ as gs) = hd l
+       and (_,gl0,_) = hd(tl l) in
+       let p = length gl - length gl0 in
+       let p' = if p < 1 then 1 else p + 1 in
+       print_xgoalstate p' gs);
+    (if (!pg_mode) then
+     let (vs,theta) =
+        if (l = []) then ([],[])
+                    else let ((vs,(_,theta,_)),_,_) = hd l in
+                         (vs,theta) in
+     let foo v =
+        let (x,_) = dest_var v in
+        x ^ if (can (rev_assoc v) theta) then " using" else " open" in
+     let xs = map foo vs in
+     (print_newline();
+      print_string "(dependent evars: ";
+      print_string_seplist ", " xs;
+      print_string ")";
+      print_newline ())));;
 
 (* ------------------------------------------------------------------------- *)
 (* Goal labelling, for fresh xgoals.                                         *)
 (* ------------------------------------------------------------------------- *)
 
 let label_goals (gs : goal list) : xgoal list =
-  let gxs = map (fun g -> (g, inc_goal_counter ())) gs in
+  let gxs = map (fun g -> inc_goal_counter (); (g, !the_goal_counter))
+                gs in
   (the_new_goal_ids := map snd gxs;
    gxs);;
 
@@ -146,7 +172,7 @@ let (xby:tactic->xrefinement) =
     (mvs',inst'),glsx',just';;
 
 (* ------------------------------------------------------------------------- *)
-(* Rotate but for xgoalstate.  Completely trivial redefinition.              *)
+(* Rotate but for xgoalstate.  Only change is different ML datatype.         *)
 (* ------------------------------------------------------------------------- *)
 
 let (xrotate:int->xrefinement) =
@@ -177,102 +203,116 @@ let (mk_xgoalstate:goal->xgoalstate) =
     else failwith "mk_goalstate: Non-boolean goal";;
 
 (* ------------------------------------------------------------------------- *)
-(* Subgoal package but for xgoals.                                           *)
+(* The Prooftree global state is an ever increasing counter.                 *)
 (* ------------------------------------------------------------------------- *)
 
-let current_xgoalstack = ref ([] :xgoalstack);;
+let the_pt_global_state = ref 1;;
 
-let (xrefine:xrefinement->xgoalstack) =
-  fun r ->
-    let l = !current_xgoalstack in
-    let h = hd l in
-    let res = r h :: l in
-    current_xgoalstack := res;
-    !current_xgoalstack;;
+let inc_pt_global_state () =
+  (the_pt_global_state := !the_pt_global_state + 1);;
 
-let flush_xgoalstack() =
-  let l = !current_xgoalstack in
-  current_xgoalstack := [hd l];;
+let pt_global_state () = !the_pt_global_state;;
 
-let xe tac =
-  the_tactic_flag := true;
-  xrefine(xby(VALID tac));;
+(* ------------------------------------------------------------------------- *)
+(* The Prooftree proof state is the length of the goal stack.                *)
+(* ------------------------------------------------------------------------- *)
 
-let xr n = xrefine(xrotate n);;
+let the_current_xgoalstack = ref ([] : goalstack);;
 
-let set_xgoal(asl,w) =
-  current_xgoalstack :=
-    [mk_xgoalstate(map (fun t -> "",ASSUME t) asl,w)];
-  !current_xgoalstack;;
+let pt_proof_state () = length !the_current_xgoalstack;;
 
-let xg t =
+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";;
+
+(* ------------------------------------------------------------------------- *)
+(* Subgoal package but for xgoals.  These overwrite the existing commands.   *)
+(* ------------------------------------------------------------------------- *)
+
+let (xrefine:xrefinement->goalstack) =
+  fun r ->
+    let l = !the_current_xgoalstack in
+    let h = hd l in
+    let res = r h :: l in
+    the_current_xgoalstack := res;
+    !the_current_xgoalstack;;
+
+let flush_goalstack() =
+  let l = !the_current_xgoalstack in
+  the_current_xgoalstack := [hd l];;
+
+let e tac =
+  let result = xrefine(xby(VALID tac)) in
+  (inc_pt_global_state ();
+   the_tactic_flag := true;
+   result);;
+
+let r n =
+  (inc_pt_global_state ();
+   xrefine(xrotate n));;
+
+let set_goal(asl,w) =
+  let aths = map ASSUME asl in
+  (inc_pt_global_state ();
+   the_current_xgoalstack :=
+     [mk_xgoalstate(map (fun th -> "",th) aths,w)];
+   !the_current_xgoalstack);;
+
+let g t =
   let fvs = sort (<) (map (fst o dest_var) (frees t)) in
   (if fvs <> [] then
      let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
      warn true ("Free variables in goal: "^errmsg)
    else ());
-   set_xgoal([],t);;
+  set_goal([],t);;
 
-let xb() =
-  let l = !current_xgoalstack in
+let b() =
+  let l = !the_current_xgoalstack in
   if length l = 1 then failwith "Can't back up any more" else
-  current_xgoalstack := tl l;
-  !current_xgoalstack;;
+  (inc_pt_global_state ();
+   the_current_xgoalstack := tl l;
+   !the_current_xgoalstack);;
 
-let xp() =
-  !current_xgoalstack;;
+let p() = !the_current_xgoalstack;;
 
-let xtop_realgoal() =
-  let (_,(((asl,w),id)::_),_)::_ = !current_xgoalstack in
+let top_realgoal() =
+  let (_,(((asl,w),id)::_),_)::_ = !the_current_xgoalstack in
   asl,w;;
 
-let xtop_goal() =
-  let asl,w = xtop_realgoal() in
+let top_goal() =
+  let asl,w = top_realgoal() in
   map (concl o snd) asl,w;;
 
-let xtop_thm() =
-  let (_,[],f)::_ = !current_xgoalstack in
+let top_thm() =
+  let (_,[],f)::_ = !the_current_xgoalstack in
   f null_inst [];;
 
 (* ------------------------------------------------------------------------- *)
-(* Goal id to goal lookup function.                                          *)
+(* Configure the annotated prompt.				             *)
 (* ------------------------------------------------------------------------- *)
 
-let print_xgoal_of_id (id:goal_id) : unit =
-  let gsts = !current_xgoalstack in
-  let find_goal (_,xgs,_) = find (fun (g,id0) -> id0 = id) xgs in
-  let xg = tryfind find_goal gsts in
-  print_xgoal xg;;
+pg_prompt_info := 
+   fun () -> 
+   let pst = pt_proof_state () and gst = pt_global_state () in
+   string_of_int gst ^ "|" ^ string_of_int pst;;
 
 (* ------------------------------------------------------------------------- *)
-(* Jumping back to a previous state.                                         *)
+(* Printing the goal of a given Prooftree goal id.                           *)
 (* ------------------------------------------------------------------------- *)
 
-let jump_back_to_state n : xgoalstack =
-  let l = length !current_xgoalstack in
-  if (0 <= n) & (n <= l)
-    then (current_xgoalstack := snd (chop_list (l-n) !current_xgoalstack);
-          !current_xgoalstack)
-    else failwith "Not a valid state number";;
+let print_xgoal_of_id (id:goal_id) : unit =
+  let gsts = !the_current_xgoalstack in
+  let find_goal (_,xgs,_) = find (fun (g,id0) -> id0 = id) xgs in
+  let xg = tryfind find_goal gsts in
+  print_xgoal xg;;
 
 (* ------------------------------------------------------------------------- *)
-(* Install the goal-related printers.                                        *)
+(* Install the new goal-related printers.                                    *)
 (* ------------------------------------------------------------------------- *)
 
 #install_printer print_xgoal;;
 #install_printer print_xgoalstack;;
-
-(* ------------------------------------------------------------------------- *)
-(* Replace the top-level prompt                                              *)
-(* ------------------------------------------------------------------------- *)
-
-(* TODO: something like this
-
-let prompt () =>
-   "[State Counter " ^ string_of_int (length (!current_xgoalstack)) ^ "]# ");
-
-Toploop.read_interactive_input := 
-  let old = !Toploop.read_interactive_input in fun prompt buffer len -> 
-     old (prompt()) buffer len ;;
-
-*)