diff options
| author | herbelin | 2005-01-14 13:07:21 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-14 13:07:21 +0000 |
| commit | 6dbc9f181b90216958fd9d87f8426901b1e4c37e (patch) | |
| tree | 637cff0f09192fdb7697b8c9cb43103589166383 | |
| parent | b1af90453f7002dec1994a0be31cfa92659496a8 (diff) | |
Affichage numéro de l'état de la commande courante pour mode emacs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6588 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/toplevel.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 36c3ff3dc7..bfbdb598a7 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -186,7 +186,10 @@ let make_prompt () = * initialized when a vernac command is immediately followed by "\n", * or after a Drop. *) let top_buffer = - let pr() = (make_prompt())^(emacs_str (String.make 1 (Char.chr 249))) + let pr() = + (make_prompt())^ + (Printer.emacs_str ("*" ^ string_of_int (Lib.current_command_label ()) ^ + String.make 1 (Char.chr 249))) in { prompt = pr; str = ""; @@ -197,7 +200,7 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt - <- (fun () -> (prompt ()) ^ (emacs_str (String.make 1 (Char.chr 249)))) + <- (fun () -> (prompt ())^(Printer.emacs_str (String.make 1 (Char.chr 249)))) (* Removes and prints the location of the error. The following exceptions need not be located. *) |