Merge branch 'trunk' into located_switch

1 files changed, 69 insertions, 44 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 3a67f4cbf..7e81aa20a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -44,7 +44,6 @@ let vernac_echo ?loc in_chan = let open Loc in
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
 
-let chan_beautify = ref stdout
 let beautify_suffix = ".beautified"
 
 let set_formatter_translator ch =
@@ -83,7 +82,9 @@ let pr_new_syntax ?loc po chan_beautify ocom =
    and a glimpse of the executed command *)
 
 let pp_cmd_header ?loc com =
-  let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
+  let shorten s =
+    if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
+  in
   let noblank s = String.map (fun c ->
       match c with
 	| ' ' | '\n' | '\t' | '\r' -> '~'
@@ -109,7 +110,17 @@ let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
   with Proof_global.NoCurrentProof -> Pp.str ""
 
-let rec interp_vernac sid po (loc,com) =
+let vernac_error msg =
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" Pp.pp_with msg;
+  flush_all ();
+  exit 1
+
+(* Reenable when we get back to feedback printing *)
+(* let is_end_of_input any = match any with *)
+(*     Stm.End_of_input -> true *)
+(*   | _ -> false *)
+
+let rec interp_vernac sid (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
@@ -117,28 +128,36 @@ let rec interp_vernac sid po (loc,com) =
         let f = Loadpath.locate_file fname in
         load_vernac verbosely sid f
     | v ->
-      try
-        let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in
-
-        (* Main STM interaction *)
-        if ntip <> `NewTip then
-          anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
-        (* Due to bug #5363 we cannot use observe here as we should,
-           it otherwise reveals bugs *)
-        (* Stm.observe nsid; *)
-        Stm.finish ();
-
-        (* We could use a more refined criteria that depends on the
-           vernac. For now we imitate the old approach. *)
-        let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
-                         not (Proof_global.there_are_pending_proofs ()) in
-
-        if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
-        nsid
-
-      with exn when CErrors.noncritical exn ->
-        ignore(Stm.edit_at sid);
-        raise exn
+
+      (* XXX: We need to run this before add as the classification is
+         highly dynamic and depends on the structure of the
+         document. Hopefully this is fixed when VtBack can be removed
+         and Undo etc... are just interpreted regularly. *)
+      let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
+        | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true
+        | _ -> false
+      in
+
+      let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
+
+      (* Main STM interaction *)
+      if ntip <> `NewTip then
+        anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
+      (* Due to bug #5363 we cannot use observe here as we should,
+         it otherwise reveals bugs *)
+      (* Stm.observe nsid; *)
+
+      let check_proof = Flags.(!compilation_mode = BuildVo || not !batch_mode) in
+      if check_proof then Stm.finish ();
+
+      (* We could use a more refined criteria that depends on the
+         vernac. For now we imitate the old approach and rely on the
+         classification. *)
+      let print_goals = not !Flags.batch_mode && not !Flags.quiet &&
+                        is_proof_step && Proof_global.there_are_pending_proofs () in
+
+      if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
+      nsid
   in
     try
       (* The -time option is only supported from console-based
@@ -147,6 +166,9 @@ let rec interp_vernac sid po (loc,com) =
       let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
     with reraise ->
+      (* XXX: In non-interactive mode edit_at seems to do very weird
+         things, so we better avoid it while we investigate *)
+      if not !Flags.batch_mode then ignore(Stm.edit_at sid);
       let (reraise, info) = CErrors.push reraise in
       let info = begin
         match Loc.get_loc info with
@@ -167,23 +189,31 @@ and load_vernac verbosely sid file =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc, ast =
+          Stm.parse_sentence !rsid in_pa
+        (* If an error in parsing occurs, we propagate the exception
+           so the caller of load_vernac will take care of it. However,
+           in the future it could be possible that we want to handle
+           all the errors as feedback events, thus in this case we
+           should relay the exception here for convenience. A
+           possibility is shown below, however we may want to refactor
+           this code:
+
         try Stm.parse_sentence !rsid in_pa
         with
-        | Stm.End_of_input -> raise Stm.End_of_input
-        | any ->
+        | any when not is_end_of_input any ->
           let (e, info) = CErrors.push any in
           let loc = Loc.get_loc info in
           let msg = CErrors.iprint (e, info) in
           Feedback.msg_error ?loc msg;
           iraise (e, info)
+       *)
       in
-
       (* Printing of vernacs *)
       if !beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
-      let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in
+      let nsid = Flags.silently (interp_vernac !rsid) (loc, ast) in
       rsid := nsid
     done;
     !rsid
@@ -209,9 +239,9 @@ and load_vernac verbosely sid file =
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-let process_expr sid po loc_ast =
+let process_expr sid loc_ast =
   checknav_deep loc_ast;
-  interp_vernac sid po loc_ast
+  interp_vernac sid loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
@@ -237,13 +267,10 @@ let chop_extension f =
 let ensure_bname src tgt =
   let src, tgt = Filename.basename src, Filename.basename tgt in
   let src, tgt = chop_extension src, chop_extension tgt in
-  if src <> tgt then begin
-    Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
-                        str "Source: " ++ str src                                                ++ fnl () ++
-                        str "Target: " ++ str tgt);
-    flush_all ();
-    exit 1
-  end
+  if src <> tgt then
+    vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
+                  str "Source: " ++ str src                                                ++ fnl () ++
+                  str "Target: " ++ str tgt)
 
 let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
 
@@ -252,17 +279,15 @@ let ensure_vo v vo = ensure ".vo" v vo
 let ensure_vio v vio = ensure ".vio" v vio
 
 let ensure_exists f =
-  if not (Sys.file_exists f) then begin
-    Feedback.msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f));
-    exit 1
-  end
+  if not (Sys.file_exists f) then
+    vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
 let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
-    if not (List.is_empty pfs) then
-      (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in
+    if not (List.is_empty pfs) then vernac_error (str "There are pending proofs")
+  in
   match !Flags.compilation_mode with
   | BuildVo ->
       let long_f_dot_v = ensure_v f in