A new status Unsafe in Interface. Meant for commands such as Admitted.

Currently :
- only Admitted uses the Unsafe return status
- the status is ignored in coqtop
- Coqide sees the status but apparently doesn't use it for colouring (I'm not
  sure why, but then again, it's not as if I understood coqide's code or
  anything)

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

6 files changed, 53 insertions, 28 deletions

diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 4537dc405..7c7738af3 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -115,9 +115,10 @@ let interp (raw,verbosely,s) =
   let loc_ast = Vernac.parse_sentence (pa,None) in
   if not raw then coqide_cmd_checks loc_ast;
   Flags.make_silent (not verbosely);
-  Vernac.eval_expr ~preserving:raw loc_ast;
+  let status = Vernac.eval_expr ~preserving:raw loc_ast in
   Flags.make_silent true;
-  read_stdout ()
+  let ret = read_stdout () in
+  if status then Util.Inl ret else Util.Inr ret
 
 (** Goal display *)
 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index ad7ad014a..cac5bd7d0 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -352,7 +352,7 @@ let do_vernac () =
   resynch_buffer top_buffer;
   begin
     try
-      raw_do_vernac top_buffer.tokens
+      ignore (raw_do_vernac top_buffer.tokens)
     with e ->
       ppnl (print_toplevel_error (process_error e))
   end;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b1d60dd4d..4cc9cacb0 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -257,22 +257,24 @@ let rec vernac_com interpfun checknav (loc,com) =
           end;
 	begin
 	  try
-	    read_vernac_file verbosely (CUnix.make_suffix fname ".v");
-	    restore_translator_coqdoc st
+	    let status = read_vernac_file verbosely (CUnix.make_suffix fname ".v") in
+	    restore_translator_coqdoc st;
+            status
 	  with e ->
 	    restore_translator_coqdoc st;
 	    raise e
 	end
 
-    | VernacList l -> List.iter (fun (_,v) -> interp v) l
+    | VernacList l ->
+        List.fold_left (fun status (_,v) -> interp v && true) true l
 
-    | v when !just_parsing -> ()
+    | v when !just_parsing -> true
 
     | VernacFail v ->
 	begin try
 	  (* If the command actually works, ignore its effects on the state *)
 	  States.with_state_protection
-	    (fun v -> interp v; raise HasNotFailed) v
+	    (fun v -> ignore (interp v); raise HasNotFailed) v
 	with e -> match real_error e with
 	  | HasNotFailed ->
 	      errorlabstrm "Fail" (str "The command has not failed !")
@@ -281,15 +283,17 @@ let rec vernac_com interpfun checknav (loc,com) =
 	      let msg = Errors.print_no_anomaly e in
 	      if_verbose msg_info
 		(str "The command has indeed failed with message:" ++
-		 fnl () ++ str "=> " ++ hov 0 msg)
+		 fnl () ++ str "=> " ++ hov 0 msg);
+              true
 	end
 
     | VernacTime v ->
 	  let tstart = System.get_time() in
-          interp v;
+          let status = interp v in
 	  let tend = get_time() in
           msg_info (str"Finished transaction in " ++
-                   System.fmt_time_difference tstart tend)
+                   System.fmt_time_difference tstart tend);
+          status
 
     | VernacTimeout(n,v) ->
 	  current_timeout := Some n;
@@ -298,9 +302,12 @@ let rec vernac_com interpfun checknav (loc,com) =
     | v ->
 	  let psh = default_set_timeout () in
 	  try
-            States.with_heavy_rollback interpfun
-              Cerrors.process_vernac_interp_error v;
-	    restore_timeout psh
+            let status =
+              States.with_heavy_rollback interpfun
+                Cerrors.process_vernac_interp_error v
+            in
+	    restore_timeout psh;
+            status
 	  with e -> restore_timeout psh; raise e
   in
     try
@@ -330,21 +337,25 @@ and read_vernac_file verbosely s =
   in
   let (in_chan, fname, input) =
     open_file_twice_if verbosely s in
+  let status = ref true in
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com interpfun checknav loc_ast;
+      let command_status = vernac_com interpfun checknav loc_ast in
+      status := !status && command_status;
       end_inner_command (snd loc_ast);
       pp_flush ()
-    done
+    done;
+    assert false
   with e ->   (* whatever the exception *)
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
     match real_error e with
       | End_of_input ->
-          if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None
+          if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None;
+          !status
       | _ -> raise_with_file fname e
 
 (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
@@ -359,9 +370,10 @@ let checknav loc ast =
     user_error loc "Navigation commands forbidden in nested commands"
 
 let eval_expr ?(preserving=false) loc_ast =
-  vernac_com Vernacentries.interp checknav loc_ast;
+  let status = vernac_com Vernacentries.interp checknav loc_ast in
   if not preserving && not (is_navigation_vernac (snd loc_ast)) then
-    Backtrack.mark_command (snd loc_ast)
+    Backtrack.mark_command (snd loc_ast);
+  status
 
 (* raw_do_vernac : Pcoq.Gram.parsable -> unit
  * vernac_step . parse_sentence *)
@@ -380,7 +392,7 @@ let load_vernac verb file =
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try
     Lib.mark_end_of_command (); (* in case we're still in coqtop init *)
-    read_vernac_file verb file;
+    let _ = read_vernac_file verb file in
     if !Flags.beautify_file then close_out !chan_beautify;
   with e ->
     if !Flags.beautify_file then close_out !chan_beautify;
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 924f2a65e..d76eb5d46 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -27,9 +27,10 @@ val just_parsing : bool ref
    Backtrack stack (triggering a save of a frozen state and the generation
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
-
-val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit
-val raw_do_vernac : Pcoq.Gram.parsable -> unit
+(* spiwack: return value: [true] if safe (general case), [false] if
+   unsafe (like [Admitted]). *)
+val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> bool
+val raw_do_vernac : Pcoq.Gram.parsable -> bool
 
 (** Set XML hooks *)
 val set_xml_start_library : (unit -> unit) -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 278e87418..142850325 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -47,6 +47,10 @@ let cl_of_qualid = function
 let scope_class_of_qualid qid =
   Notation.scope_class_of_reference (Smartlocate.smart_global qid)
 
+(** Vernac commands can raise this [UnsafeSuccess] to notify they
+    modified the environment in an unsafe manner, such as [Admitted]. *)
+exception UnsafeSuccess
+
 (*******************)
 (* "Show" commands *)
 
@@ -475,7 +479,8 @@ let qed_display_script = ref true
 let vernac_end_proof = function
   | Admitted ->
     Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
-    admit ()
+    admit ();
+    raise UnsafeSuccess
   | Proved (is_opaque,idopt) ->
     let prf = Pfedit.get_current_proof_name () in
     if is_verbose () && !qed_display_script then show_script ();
@@ -1734,8 +1739,13 @@ let interp c =
   Obligations.set_program_mode isprogcmd;
   try
     interp c; Locality.check_locality ();
-    Flags.program_mode := mode
-  with e ->
+    Flags.program_mode := mode;
+    true
+  with
+    | UnsafeSuccess ->
+        Flags.program_mode := mode;
+        false
+    | e ->
     Flags.program_mode := mode;
     raise e
 
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 98f0f1ab3..dbceaaaa1 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -25,8 +25,9 @@ val show_node : unit -> unit
 val get_current_context_of_args : int option -> Evd.evar_map * Environ.env
 
 (** The main interpretation function of vernacular expressions *)
-
-val interp : Vernacexpr.vernac_expr -> unit
+(* spiwack: return value: [true] if safe (general case), [false] if
+   unsafe (like [Admitted]). *)
+val interp : Vernacexpr.vernac_expr -> bool
 
 (** Print subgoals when the verbose flag is on.
     Meant to be used inside vernac commands from plugins. *)