diff options
| author | vgross | 2009-10-05 16:21:01 +0000 |
|---|---|---|
| committer | vgross | 2009-10-05 16:21:01 +0000 |
| commit | 02a8749f2be324b2fe85897af17d9943dfcd08d7 (patch) | |
| tree | 1f3cf3ac1394da17fed781d183c912c5e2c088fe /toplevel | |
| parent | 3b57619bd5dc164dcb51ad4fb390efd258940917 (diff) | |
Revert "kills the old backtracking framework and replaces it with"
This reverts commit 33545cc88bf4b4e19b222afd2d1d264bcba97838.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12373 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/toplevel.ml | 19 | ||||
| -rw-r--r-- | toplevel/toplevel.mli | 4 |
2 files changed, 9 insertions, 14 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index c9f2a87723..d14acaab9c 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -224,13 +224,6 @@ 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 @@ -240,9 +233,15 @@ let current_status_triple () = "n |lem1|lem2|lem3| p < " *) let make_emacs_prompt() = - 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 + 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 ^ " < " else "" (* A buffer to store the current command read on stdin. It is diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index 8204660f2f..3f2fa83adb 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -44,7 +44,3 @@ val do_vernac : unit -> unit (* Main entry point of Coq: read and execute vernac commands. *) val loop : unit -> unit - -(* hack to handle backtracking in CoqIde *) - -val current_status_triple : unit -> int * string list * int |