From c555e8464414a42c33235f31c84545a86290eb31 Mon Sep 17 00:00:00 2001 From: vgross Date: Tue, 29 Sep 2009 11:26:49 +0000 Subject: kills the old backtracking framework and replaces it with ProofGeneral-like "Backtrack". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12364 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/toplevel.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'toplevel/toplevel.ml') diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index d14acaab9..c9f2a8772 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -224,6 +224,13 @@ let make_prompt () = "<"^l' *) +let current_status_triple () = + let statnum = Lib.current_command_label () in + let dpth = Pfedit.current_proof_depth () in + let pf_info = if 0 <= dpth then dpth else 0 in + let pending = List.map Names.string_of_id (Pfedit.get_all_proof_names ()) in + (statnum,pending,pf_info) + (* the coq prompt added to the default one when in emacs mode The prompt contains the current state label [n] (for global backtracking) and the current proof state [p] (for proof @@ -233,15 +240,9 @@ let make_prompt () = "n |lem1|lem2|lem3| p < " *) let make_emacs_prompt() = - let statnum = string_of_int (Lib.current_command_label ()) in - let dpth = Pfedit.current_proof_depth() in - let pending = Pfedit.get_all_proof_names() in - let pendingprompt = - List.fold_left - (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) - "" pending in - let proof_info = if dpth >= 0 then string_of_int dpth else "0" in - if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " + let statnum,pending,proof_info = current_status_triple () in + let pendingprompt = String.concat "|" pending in + if !Flags.print_emacs then Printf.sprintf "%d |%s| %d < " statnum pendingprompt proof_info else "" (* A buffer to store the current command read on stdin. It is -- cgit v1.2.3