Toplevel: improved comments

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16295 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 14 insertions, 10 deletions

diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 1a318e5e18..9a2b8840c7 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -292,11 +292,15 @@ let read_sentence () =
   try Vernac.parse_sentence (top_buffer.tokens, None)
   with reraise -> discard_to_dot (); raise reraise
 
-(* do_vernac reads and executes a toplevel phrase, and print error
-   messages when an exception is raised, except for the following:
-     Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
+(** [do_vernac] reads and executes a toplevel phrase, and print error
+    messages when an exception is raised, except for the following:
+    - Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
            Otherwise, exit.
-     End_of_input: Ctrl-D was typed in, we will quit *)
+    - End_of_input: Ctrl-D was typed in, we will quit.
+
+    In particular, this is normally the only place where a Sys.Break
+    is catched and handled (i.e. not re-raised).
+*)
 
 let do_vernac () =
   msgerrnl (mt ());
@@ -311,11 +315,11 @@ let do_vernac () =
         else ppnl (str"Error: There is no ML toplevel." ++ fnl ())
     | any -> ppnl (print_toplevel_error any)
 
-(* coq and go read vernacular expressions until Drop is entered.
- * Ctrl-C will raise the exception Break instead of aborting Coq.
- * Here we catch the exceptions terminating the Coq loop, and decide
- * if we really must quit.
- *)
+(** Main coq loop : read vernacular expressions until Drop is entered.
+    Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
+    Normally, the only exceptions that can come out of [do_vernac] and
+    exit the loop are Drop and Quit. Any other exception there indicates
+    an issue with [print_toplevel_error] above. *)
 
 let rec loop () =
   Sys.catch_break true;
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 0af05d02f7..1375f33619 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -33,7 +33,7 @@ val set_prompt : (unit -> string) -> unit
 
 val print_toplevel_error : exn -> std_ppcmds
 
-(** Parse and execute a vernac command. *)
+(** Parse and execute one vernac command. *)
 
 val do_vernac : unit -> unit