Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 355 insertions, 156 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index d318e339..5166fb21 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 10174 2007-10-04 13:52:23Z vsiles $ *)
+(* $Id: coq.ml 11126 2008-06-13 18:45:04Z herbelin $ *)
 
 open Vernac
 open Vernacexpr
@@ -43,33 +43,38 @@ let init () =
      Problem: should not hide "xx is assumed"
      messages *)
 (**)
-  Options.make_silent true;
+  Flags.make_silent true;
 (**)
   Coqtop.init_ide ()
 
 
 let i = ref 0
 
-let version () =
+let get_version_date () =
   let date =
     if Glib.Utf8.validate Coq_config.date
     then Coq_config.date
     else "<date not printable>" in
-  let get_version_date () =
-    try
-      let ch = open_in (Coq_config.coqtop^"/revision") in
-      let ver = input_line ch in
-      let rev = input_line ch in
-	(ver,rev)
-    with _ -> (Coq_config.version,date) in
-  let (rev,ver) = get_version_date () in
+  try
+    let ch = open_in (Coq_config.coqtop^"/revision") in
+    let ver = input_line ch in
+    let rev = input_line ch in
+    (ver,rev)
+  with _ -> (Coq_config.version,date)
+
+let short_version () =
+  let (ver,date) = get_version_date () in
+  Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date
+
+let version () =
+  let (ver,date) = get_version_date () in
     Printf.sprintf 
       "The Coq Proof Assistant, version %s (%s)\
        \nArchitecture %s running %s operating system\
        \nGtk version is %s\
        \nThis is the %s version (%s is the best one for this architecture and OS)\
        \n"
-      rev ver
+      ver date
       Coq_config.arch Sys.os_type
       (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
     (if Mltop.get () = Mltop.Native then "native" else "bytecode") 
@@ -110,7 +115,310 @@ let is_in_proof_mode () =
 let user_error_loc l s =
   raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
 
-let interp verbosely s = 
+type printing_state = {
+  mutable printing_implicit : bool;
+  mutable printing_coercions : bool;
+  mutable printing_raw_matching : bool;
+  mutable printing_no_notation : bool;
+  mutable printing_all : bool;
+  mutable printing_evar_instances : bool;
+  mutable printing_universes : bool;
+  mutable printing_full_all : bool
+}
+
+let printing_state = {
+  printing_implicit = false;
+  printing_coercions = false;
+  printing_raw_matching = false;
+  printing_no_notation = false;
+  printing_all = false;
+  printing_evar_instances = false;
+  printing_universes = false;
+  printing_full_all = false;
+}
+
+let printing_implicit_data = ["Printing";"Implicit"], false
+let printing_coercions_data = ["Printing";"Coercions"], false
+let printing_raw_matching_data = ["Printing";"Matching"], true
+let printing_no_synth_data = ["Printing";"Synth"], true
+let printing_no_notation_data = ["Printing";"Notations"], true
+let printing_all_data = ["Printing";"All"], false
+let printing_evar_instances_data = ["Printing";"Existential";"Instances"],false
+let printing_universes_data = ["Printing";"Universes"], false
+
+let known_options = ref []
+
+let prepare_option (l,dft) =
+  known_options := l :: !known_options;
+  let set = (String.concat " " ("Set"::l)) ^ "." in
+  let unset = (String.concat " " ("Unset"::l)) ^ "." in
+  if dft then unset,set else set,unset
+
+let coqide_known_option = function
+  | Goptions.TertiaryTable (a,b,c) -> List.mem [a;b;c] !known_options
+  | Goptions.SecondaryTable (a,b) -> List.mem [a;b] !known_options
+  | Goptions.PrimaryTable a -> List.mem [a] !known_options
+
+let with_printing_implicit = prepare_option printing_implicit_data
+let with_printing_coercions = prepare_option printing_coercions_data
+let with_printing_raw_matching = prepare_option printing_raw_matching_data
+let with_printing_no_synth = prepare_option printing_no_synth_data
+let with_printing_no_notation = prepare_option printing_no_notation_data
+let with_printing_all = prepare_option printing_all_data
+let with_printing_evar_instances = prepare_option printing_evar_instances_data
+let with_printing_universes = prepare_option printing_universes_data
+
+let make_option_commands () =
+  let p = printing_state in
+  (if p.printing_implicit then [with_printing_implicit] else [])@
+  (if p.printing_coercions then [with_printing_coercions] else [])@
+  (if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@
+  (if p.printing_no_notation then [with_printing_no_notation] else [])@
+  (if p.printing_all then [with_printing_all] else [])@
+  (if p.printing_evar_instances then [with_printing_evar_instances] else [])@
+  (if p.printing_universes then [with_printing_universes] else [])@
+  (if p.printing_full_all then [with_printing_all;with_printing_evar_instances;with_printing_universes] else [])
+
+let make_option_commands () =
+  let l = make_option_commands () in
+  List.iter (fun (a,b) -> prerr_endline a; prerr_endline b) l;
+  l
+
+type command_attribute =
+    NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand
+  | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
+  | ProofEndingCommand
+
+let rec attribute_of_vernac_command = function
+  (* Control *)
+  | VernacTime com -> attribute_of_vernac_command com
+  | VernacList _ -> [] (* unsupported *)
+  | VernacLoad _ -> []
+
+  (* Syntax *)
+  | VernacTacticNotation _ -> []
+  | VernacSyntaxExtension _ -> []
+  | VernacDelimiters _ -> []
+  | VernacBindScope _ -> []
+  | VernacOpenCloseScope _ -> []
+  | VernacArgumentsScope _ -> []
+  | VernacInfix _ -> []
+  | VernacNotation _ -> []
+
+  (* Gallina *)
+  | VernacDefinition (_,_,DefineBody _,_) -> []
+  | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
+  | VernacStartTheoremProof _ -> [GoalStartingCommand]
+  | VernacEndProof _ -> [ProofEndingCommand]
+  | VernacExactProof _ -> [ProofEndingCommand]
+
+  | VernacAssumption _ -> []
+  | VernacInductive _ -> []
+  | VernacFixpoint _ -> []
+  | VernacCoFixpoint _ -> []
+  | VernacScheme _ -> []
+  | VernacCombinedScheme _ -> []
+
+  (* Modules *)
+  | VernacDeclareModule _ -> []
+  | VernacDefineModule _  -> []
+  | VernacDeclareModuleType _ -> []
+  | VernacInclude _ -> []
+
+  (* Gallina extensions *)
+  | VernacBeginSection _ -> []
+  | VernacEndSegment _ -> []
+  | VernacRecord _ -> []
+  | VernacRequire _ -> []
+  | VernacImport _ -> []
+  | VernacCanonical _ -> []
+  | VernacCoercion _ -> []
+  | VernacIdentityCoercion _ -> []
+
+  (* Type classes *)
+  | VernacClass _ -> []
+  | VernacInstance _ -> []
+  | VernacContext _ -> []
+  | VernacDeclareInstance _ -> []
+
+  (* Solving *)
+  | VernacSolve _ -> [SolveCommand]
+  | VernacSolveExistential _ -> [SolveCommand]
+
+  (* MMode *)
+  | VernacDeclProof -> []
+  | VernacReturn -> []
+  | VernacProofInstr _ -> []
+
+  (* Auxiliary file and library management *)
+  | VernacRequireFrom _ -> []
+  | VernacAddLoadPath _ -> []
+  | VernacRemoveLoadPath _ -> []
+  | VernacAddMLPath _ -> []
+  | VernacDeclareMLModule _ -> []
+  | VernacChdir _ -> [OtherStatePreservingCommand]
+
+  (* State management *)
+  | VernacWriteState _ -> []
+  | VernacRestoreState _ -> []
+
+  (* Resetting *)
+  | VernacRemoveName _ -> [NavigationCommand]
+  | VernacResetName _ -> [NavigationCommand]
+  | VernacResetInitial -> [NavigationCommand]
+  | VernacBack _ -> [NavigationCommand]
+  | VernacBackTo _ -> [NavigationCommand]
+
+  (* Commands *)
+  | VernacDeclareTacticDefinition _ -> []
+  | VernacHints _ -> []
+  | VernacSyntacticDefinition _ -> []
+  | VernacDeclareImplicits _ -> []
+  | VernacReserve _ -> []
+  | VernacSetOpacity _ -> []
+  | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) -> 
+      [DebugCommand]
+  | VernacSetOption (o,BoolValue true) | VernacUnsetOption o ->
+      if coqide_known_option o then [KnownOptionCommand] else []
+  | VernacSetOption _ -> []
+  | VernacRemoveOption _ -> []
+  | VernacAddOption _ -> []
+  | VernacMemOption _ -> [QueryCommand]
+
+  | VernacPrintOption _ -> [QueryCommand]
+  | VernacCheckMayEval _ -> [QueryCommand]
+  | VernacGlobalCheck _ -> [QueryCommand]
+  | VernacPrint _ -> [QueryCommand]
+  | VernacSearch _ -> [QueryCommand]
+  | VernacLocate _ -> [QueryCommand]
+
+  | VernacComments _ -> [OtherStatePreservingCommand]
+  | VernacNop -> [OtherStatePreservingCommand]
+
+  (* Proof management *)
+  | VernacGoal _ -> [GoalStartingCommand]
+
+  | VernacAbort _ -> [NavigationCommand]
+  | VernacAbortAll -> [NavigationCommand]
+  | VernacRestart -> [NavigationCommand]
+  | VernacSuspend -> [NavigationCommand]
+  | VernacResume _ -> [NavigationCommand]
+  | VernacUndo _ -> [NavigationCommand]
+  | VernacUndoTo _ -> [NavigationCommand]
+  | VernacBacktrack _ -> [NavigationCommand]
+
+  | VernacFocus _ -> [SolveCommand]
+  | VernacUnfocus -> [SolveCommand]
+  | VernacGo _ -> []
+  | VernacShow _ -> [OtherStatePreservingCommand]
+  | VernacCheckGuard -> [OtherStatePreservingCommand]
+  | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
+  | VernacProof _ -> []
+
+  (* Toplevel control *)
+  | VernacToplevelControl _ -> []
+
+  (* Extensions *)
+  | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
+  | VernacExtend _ -> []
+
+let is_vernac_goal_starting_command com =
+  List.mem GoalStartingCommand (attribute_of_vernac_command com)
+
+let is_vernac_navigation_command com =
+  List.mem NavigationCommand (attribute_of_vernac_command com)
+
+let is_vernac_query_command com =
+  List.mem QueryCommand (attribute_of_vernac_command com)
+
+let is_vernac_known_option_command com =
+  List.mem KnownOptionCommand (attribute_of_vernac_command com)
+
+let is_vernac_debug_command com =
+  List.mem DebugCommand (attribute_of_vernac_command com)
+
+let is_vernac_goal_printing_command com =
+  let attribute = attribute_of_vernac_command com in
+  List.mem GoalStartingCommand attribute or
+  List.mem SolveCommand attribute
+
+let is_vernac_state_preserving_command com =
+  let attribute = attribute_of_vernac_command com in
+  List.mem OtherStatePreservingCommand attribute or
+  List.mem QueryCommand attribute
+
+let is_vernac_tactic_command com =
+  List.mem SolveCommand (attribute_of_vernac_command com)
+
+let is_vernac_proof_ending_command com =
+  List.mem ProofEndingCommand (attribute_of_vernac_command com)
+
+type undo_info = identifier list
+
+let undo_info () = Pfedit.get_all_proof_names ()
+
+type reset_mark =
+  | ResetToId of Names.identifier     (* Relying on identifiers only *)
+  | ResetToState of Libnames.object_name (* Relying on states if any *)
+
+type reset_status =
+  | NoReset
+  | ResetAtSegmentStart of Names.identifier
+  | ResetAtRegisteredObject of reset_mark
+
+type reset_info = reset_status * undo_info * bool ref
+
+
+let reset_mark id = match Lib.has_top_frozen_state () with
+  | Some sp -> 
+      prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
+      ResetToState sp
+  | None -> ResetToId id
+
+let compute_reset_info = function 
+  | VernacBeginSection id 
+  | VernacDefineModule (_,id, _, _, _) 
+  | VernacDeclareModule (_,id, _, _)
+  | VernacDeclareModuleType (id, _, _) ->
+      ResetAtSegmentStart (snd id), undo_info(), ref true
+
+  | VernacDefinition (_, (_,id), DefineBody _, _)
+  | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
+  | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
+      ResetAtRegisteredObject (reset_mark id), undo_info(), ref true
+
+  | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true
+  | VernacEndSegment _ -> NoReset, undo_info(), ref true
+
+  | com when is_vernac_tactic_command com -> NoReset, undo_info(), ref true
+  | _ ->
+      (match Lib.has_top_frozen_state () with
+      | Some sp -> 
+	  prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
+	  ResetAtRegisteredObject (ResetToState sp)
+      | None -> NoReset), undo_info(), ref true
+
+let reset_initial () = 
+  prerr_endline "Reset initial called"; flush stderr;
+  Vernacentries.abort_refine Lib.reset_initial ()
+
+let reset_to = function
+  | ResetToId id ->
+      prerr_endline ("Reset called with "^(string_of_id id));
+      Lib.reset_name (Util.dummy_loc,id)
+  | ResetToState sp ->
+      prerr_endline
+        ("Reset called with state "^(Libnames.string_of_path (fst sp)));
+      Lib.reset_to_state sp
+
+let reset_to_mod id = 
+  prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); 
+  Lib.reset_mod (Util.dummy_loc,id)
+
+let raw_interp s =
+  Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s))
+
+let interp_with_options verbosely options s = 
   prerr_endline "Starting interp...";
   prerr_endline s;
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
@@ -118,48 +426,28 @@ let interp verbosely s =
   match pe with 
     | None -> assert false
     | Some((loc,vernac) as last) ->
-	match vernac with
-	  | VernacDefinition _  | VernacStartTheoremProof _ 
-	  | VernacBeginSection _ | VernacGoal _
-	  | VernacDefineModule _ | VernacDeclareModuleType _
-	  | VernacDeclareTacticDefinition _
-		when is_in_proof_mode () -> 
-		  user_error_loc loc (str "CoqIDE do not support nested goals")
-	  | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) ->
-	      user_error_loc loc (str "Debug mode not available within CoqIDE")
-	  | VernacResetName _
-	  | VernacResetInitial 
-	  | VernacBack _ 
-	  | VernacAbort _ 
-	  | VernacAbortAll
-	  | VernacRestart
-	  | VernacSuspend
-	  | VernacResume _
-	  | VernacUndo _ ->
-	      user_error_loc loc (str "Use CoqIDE navigation instead") 
-	  | _ ->
-	      begin
-		match vernac with
-		  | VernacPrintOption _ 
-		  | VernacCheckMayEval _
-		  | VernacGlobalCheck _
-		  | VernacPrint _
-		  | VernacSearch _ 
-		    -> !flash_info 
-			"Warning: query commands should not be inserted in scripts" 
-		  | VernacDefinition (_,_,DefineBody _,_) 
-		  | VernacInductive _
-		  | VernacFixpoint _
-		  | VernacCoFixpoint _
-		  | VernacEndProof _
-                  | VernacScheme _ 
-		    -> Options.make_silent (not verbosely)
-		  | _ -> ()
-	      end;
-	      Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
-	      Options.make_silent true;
-	      prerr_endline ("...Done with interp of : "^s);
-	      last
+	if is_vernac_debug_command vernac then
+	  user_error_loc loc (str "Debug mode not available within CoqIDE");
+	if is_vernac_navigation_command vernac then
+	  user_error_loc loc (str "Use CoqIDE navigation instead");
+	if is_vernac_known_option_command vernac then
+	  user_error_loc loc (str "Use CoqIDE display menu instead");
+	if is_vernac_query_command vernac then 
+	  !flash_info
+	    "Warning: query commands should not be inserted in scripts";
+	if not (is_vernac_goal_printing_command vernac) then
+	  (* Verbose if in small step forward and not a tactic *)
+	  Flags.make_silent (not verbosely);
+	let reset_info = compute_reset_info vernac in
+	List.iter (fun (set_option,_) -> raw_interp set_option) options;
+	raw_interp s;
+	Flags.make_silent true;
+	List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
+	prerr_endline ("...Done with interp of : "^s);
+	reset_info,last
+
+let interp verbosely phrase =
+  interp_with_options verbosely (make_option_commands ()) phrase
 
 let interp_and_replace s = 
   let result = interp false s in
@@ -196,11 +484,6 @@ let try_interptac s =
   | Stdpp.Exc_located (_,e) -> prerr_endline ("try_interp: failed ("^(Printexc.to_string e)); Failed
   | e -> Failed	  
 
-let is_tactic = function
-  | VernacSolve _ -> true
-  | _ -> false
-
-
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e
@@ -238,7 +521,8 @@ let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
 let interp_last last = 
   prerr_string "*";
   try
-    vernac_com (States.with_heavy_rollback Vernacentries.interp) last
+    vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
+    Lib.add_frozen_state()
   with e ->
     let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
     raise e
@@ -265,29 +549,25 @@ let prepare_hyps sigma env =
   in
   List.rev hyps
 
-let prepare_goal sigma g =
+let prepare_goal_main sigma g =
   let env = evar_env g in
   (prepare_hyps sigma env,
    (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl)))
 
-let prepare_meta sigma env (m,typ)  =
-  env, sigma, 
-  (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ))
-
-let prepare_metas info sigma env =
-  List.fold_right 
-    (fun cpl acc ->  
-      let meta = prepare_meta sigma env cpl in meta :: acc)
-    info.pm_subgoals [] 
+let prepare_goal sigma g =
+  let options = make_option_commands () in
+  List.iter (fun (set_option,_) -> raw_interp set_option) options;
+  let x = prepare_goal_main sigma g in
+  List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
+  x
 
 let get_current_pm_goal () =
   let pfts = get_pftreestate ()  in
   let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in
-  let info = Decl_mode.get_info gls.it in
-  let env = pf_env gls in
   let sigma= sig_sig gls in
-    (prepare_hyps sigma env,
-     prepare_metas info sigma env)
+  let gl = sig_it gls in
+    prepare_goal sigma gl
+
 
 let get_current_goals () = 
     let pfts = get_pftreestate () in
@@ -306,75 +586,6 @@ let print_no_goal () =
     msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls)
 
 
-type word_class = Normal | Kwd | Reserved
-
-
-let kwd = [(* "Compile";"Inductive";"Qed";"Type";"end";"Axiom";
-	      "Definition";"Load";"Quit";"Variable";"in";"Cases";"FixPoint";
-	      "Parameter";"Set";"of";"CoFixpoint";"Grammar";"Proof";"Syntax";
-	      "using";"CoInductive";"Hypothesis";"Prop";"Theorem";
-	   *)
-  "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
-  "CoInductive"; "Defined"; "Definition"; 
-  "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
-  "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; 
-  "Infix"; "Lemma"; "Load"; "Local"; 
-  "Match"; "Module"; "Module Type";
-  "Mutual"; "Parameter"; "Print"; "Proof"; "Qed";
-  "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
-  "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-  "Unset"; "Variable"; "Variables"; 
-]
-	    
-let reserved = []
-
-module SHashtbl = 
-  Hashtbl.Make 
-    (struct 
-       type t = string
-       let equal = ( = )
-       let hash = Hashtbl.hash
-     end)
-
-
-let word_tbl = SHashtbl.create 37
-let _ = 
-  List.iter (fun w -> SHashtbl.add word_tbl w Kwd) kwd;
-  List.iter (fun w -> SHashtbl.add word_tbl w Reserved) reserved
-
-let word_class s = 
-  try
-    SHashtbl.find word_tbl s
-  with Not_found -> Normal
-
-type reset_info = NoReset | Reset of Names.identifier * bool ref
-
-let compute_reset_info = function 
-  | VernacDefinition (_, (_,id), DefineBody _, _) 
-  | VernacBeginSection (_,id) 
-  | VernacDefineModule (_,(_,id), _, _, _) 
-  | VernacDeclareModule (_,(_,id), _, _)
-  | VernacDeclareModuleType ((_,id), _, _)
-  | VernacAssumption (_, (_,((_,id)::_,_))::_)
-  | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
-      Reset (id, ref true)
-  | VernacDefinition (_, (_,id), ProveBody _, _)
-  | VernacStartTheoremProof (_, (_,id), _, _, _) ->
-      Reset (id, ref false)
-  | _ -> NoReset
-
-let reset_initial () = 
-  prerr_endline "Reset initial called"; flush stderr;
-  Vernacentries.abort_refine Lib.reset_initial ()
-
-let reset_to id = 
-  prerr_endline ("Reset called with "^(string_of_id id));
-  Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id)
-let reset_to_mod id = 
-  prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); 
-  Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id)
-
-
 let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
   [("clear "^ident),("clear "^ident^".");
    
@@ -480,21 +691,9 @@ let make_cases s =
 	  []
     | _ -> raise Not_found
 
-let is_state_preserving = function
-  | VernacPrint _ | VernacPrintOption _ | VernacGlobalCheck _
-  | VernacCheckMayEval _ | VernacSearch _ | VernacLocate _ 
-  | VernacShow _ | VernacMemOption _ | VernacComments _ 
-  | VernacChdir None | VernacNop -> 
-      prerr_endline "state preserving command found"; true
-  | _ -> 
-      false
-
-
 let current_status () = 
   let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
   let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
   try
     path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
   with _ -> path
-
-