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

10 files changed, 96 insertions, 59 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 9c6baee693..fb9ef53661 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -631,14 +631,14 @@ object(self)
     match Coq.goals handle with
     | Interface.Fail (l, str) ->
       self#set_message ("Error in coqtop:\n"^str)
-    | Interface.Good goals ->
+    | Interface.Good goals | Interface.Unsafe goals ->
       begin match Coq.evars handle with
-      | Interface.Fail (l, str) ->
+      | Interface.Fail (l, str)->
         self#set_message ("Error in coqtop:\n"^str)
-      | Interface.Good evs ->
+      | Interface.Good evs  | Interface.Unsafe evs ->
         let hints = match Coq.hints handle with
         | Interface.Fail (_, _) -> None
-        | Interface.Good hints -> hints
+        | Interface.Good hints | Interface.Unsafe hints -> hints
         in
         Ideproof.display (Ideproof.mode_tactic menu_callback)
           proof_view goals hints evs
@@ -654,7 +654,7 @@ object(self)
     in
     match Coq.interp handle self#push_message ~raw:true ~verbose:false phrase with
     | Interface.Fail (_, err) -> sync display_error err
-    | Interface.Good msg -> sync self#insert_message msg
+    | Interface.Good msg | Interface.Unsafe msg -> sync self#insert_message msg
 
   method private find_phrase_starting_at (start:GText.iter) =
     try
@@ -705,7 +705,7 @@ object(self)
         let phrase = start#get_slice ~stop in
         match Coq.interp handle push_info ~verbose phrase with
         | Interface.Fail (loc, msg) -> error := Some (phrase, loc, msg);
-        | Interface.Good msg -> push_info Interface.Notice msg
+        | Interface.Good msg | Interface.Unsafe msg -> push_info Interface.Notice msg
       end;
       (* If there is no error, then we mark it done *)
       if !error = None then begin
@@ -812,7 +812,7 @@ object(self)
   (** Actually performs the undoing *)
   method private undo_command_stack handle n =
     match Coq.rewind handle n with
-    | Interface.Good n ->
+    | Interface.Good n | Interface.Unsafe n ->
       let until _ len _ _ = n <= len in
       (* Coqtop requested [n] more ACTUAL backtrack *)
       ignore (self#clear_command_stack until)
@@ -862,8 +862,7 @@ object(self)
       match Coq.interp handle default_logger ~verbose:false phrase with
         | Interface.Fail (l,str) -> sync display_error (l,str); None
         | Interface.Good msg -> sync self#insert_message msg; Some Safe
-          (* TODO: Restore someday the access to Decl_mode.get_damon_flag,
-             and also detect the use of admit, and then return Unsafe *)
+        | Interface.Unsafe msg -> sync self#insert_message msg; Some Unsafe
 
   method private insert_this_phrase_on_success handle coqphrase insertphrase =
     let mark_processed safe =
@@ -935,13 +934,13 @@ object(self)
 	  | Interface.Fail (_,str) ->
 	    self#set_message
 	      ("Could not determine lodpath, this might lead to problems:\n"^str)
-	  | Interface.Good true -> ()
-	  | Interface.Good false ->
+	  | Interface.Good true | Interface.Unsafe true -> ()
+	  | Interface.Good false | Interface.Unsafe false ->
 	    let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
 	    match Coq.interp handle default_logger cmd with
 	      | Interface.Fail (l,str) ->
 		self#set_message ("Couln't add loadpath:\n"^str)
-	      | Interface.Good _ -> ()
+	      | Interface.Good _ | Interface.Unsafe _ -> ()
 
   method help_for_keyword () =
     browse_keyword (self#insert_message) (get_current_word ())
@@ -1586,7 +1585,7 @@ let main files =
         let msg = match Coq.status handle with
         | Interface.Fail (l, str) ->
           "Oops, problem while fetching coq status."
-        | Interface.Good status ->
+        | Interface.Good status | Interface.Unsafe status ->
           let path = match status.Interface.status_path with
           | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
           | _ :: l -> " in " ^ String.concat "." l
@@ -1611,7 +1610,7 @@ let main files =
     try
       Coq.try_grab coqtop begin fun handle -> match Coq.mkcases handle w with
         | Interface.Fail _ -> raise Not_found
-        | Interface.Good cases ->
+        | Interface.Good cases | Interface.Unsafe cases ->
           let print_branch c l =
 	    Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
 	      (print_list (fun c s -> Format.fprintf c "%s@ " s)) l
diff --git a/lib/interface.mli b/lib/interface.mli
index 1b9c2c6389..8511bffc84 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -117,4 +117,5 @@ type location = (int * int) option (* start and end of the error *)
 
 type 'a value =
   | Good of 'a
+  | Unsafe of 'a
   | Fail of (location * string)
diff --git a/lib/serialize.ml b/lib/serialize.ml
index ed595c3146..9abb5aa6b5 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -40,7 +40,8 @@ type 'a call =
 (** The structure that coqtop should implement *)
 
 type handler = {
-  interp : raw * verbose * string -> string;
+  (* spiwack: [Inl] for safe and [Inr] for unsafe. *)
+  interp : raw * verbose * string -> (string,string) Util.union;
   rewind : int -> int;
   goals : unit -> goals option;
   evars : unit -> evar list option;
@@ -76,21 +77,28 @@ let quit : unit call = Quit
 
 let abstract_eval_call handler c =
   try
-    let res = match c with
-      | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string)
-      | Rewind i -> Obj.magic (handler.rewind i : int)
-      | Goal -> Obj.magic (handler.goals () : goals option)
-      | Evars -> Obj.magic (handler.evars () : evar list option)
-      | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
-      | Status -> Obj.magic (handler.status () : status)
-      | Search flags -> Obj.magic (handler.search flags : search_answer list)
-      | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
-      | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
-      | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
-      | MkCases s -> Obj.magic (handler.mkcases s : string list list)
-      | Quit -> Obj.magic (handler.quit () : unit)
-      | About -> Obj.magic (handler.about () : coq_info)
-    in Good res
+    match c with
+      | Interp (r,b,s) ->
+          begin match handler.interp (r,b,s) with
+            | Util.Inl v -> Good (Obj.magic (v:string))
+            | Util.Inr v -> Unsafe (Obj.magic (v:string))
+          end
+      | c ->
+          let res = match c with
+            | Interp (r,b,s) -> assert false
+            | Rewind i -> Obj.magic (handler.rewind i : int)
+            | Goal -> Obj.magic (handler.goals () : goals option)
+            | Evars -> Obj.magic (handler.evars () : evar list option)
+            | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
+            | Status -> Obj.magic (handler.status () : status)
+            | Search flags -> Obj.magic (handler.search flags : search_answer list)
+            | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
+            | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
+            | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
+            | MkCases s -> Obj.magic (handler.mkcases s : string list list)
+            | Quit -> Obj.magic (handler.quit () : unit)
+            | About -> Obj.magic (handler.about () : coq_info)
+          in Good res
   with e ->
     let (l, str) = handler.handle_exn e in
     Fail (l,str)
@@ -253,6 +261,7 @@ let to_search_answer = function
 
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
+| Unsafe x -> Element ("value", ["val", "unsafe"], [f x])
 | Fail (loc, msg) ->
   let loc = match loc with
   | None -> []
@@ -264,6 +273,7 @@ let to_value f = function
 | Element ("value", attrs, l) ->
   let ans = massoc "val" attrs in
   if ans = "good" then Good (f (singleton l))
+  else if ans = "unsafe" then Unsafe (f (singleton l))
   else if ans = "fail" then
     let loc =
       try
@@ -533,6 +543,7 @@ let pr_call = function
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
+  | Unsafe v -> "UNSAFE" ^ pr v
   | Fail (_,str) -> "FAIL ["^str^"]"
 
 let pr_value v = pr_value_gen (fun _ -> "") v
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 8b24aca156..4ad30c72de 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -76,7 +76,8 @@ val quit : unit call
 (** The structure that coqtop should implement *)
 
 type handler = {
-  interp : raw * verbose * string -> string;
+  (* spiwack: [Inl] for safe and [Inr] for unsafe. *)
+  interp : raw * verbose * string -> (string,string) Util.union;
   rewind : int -> int;
   goals : unit -> goals option;
   evars : unit -> evar list option;
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 4537dc405d..7c7738af38 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 ad7ad014a9..cac5bd7d00 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 b1d60dd4d7..4cc9cacb05 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 924f2a65e9..d76eb5d46e 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 278e874183..1428503251 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 98f0f1ab3b..dbceaaaa1e 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. *)