Merge branch 'trunk' into located_switch

6 files changed, 122 insertions, 89 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index ab360f98d..ab5104c78 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -148,19 +148,6 @@ let print_highlight_location ib loc =
 let valid_buffer_loc ib loc =
   let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
 
-(* This is specific to the toplevel *)
-let pr_loc ?loc = Option.default (fun loc ->
-    let fname = loc.Loc.fname in
-    if CString.equal fname "" then
-      Loc.(str"Toplevel input, characters " ++ int loc.bp ++
-	   str"-" ++ int loc.ep ++ str":")
-    else
-      Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
-	   str", line " ++ int loc.line_nb ++ str", characters " ++
-	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
-	   str":")
-  ) loc
-
 (* Toplevel error explanation. *)
 let error_info_for_buffer ?loc buf =
   Option.map (fun loc ->
@@ -175,7 +162,7 @@ let error_info_for_buffer ?loc buf =
           else (mt (), nloc)
           (* we are in batch mode, don't adjust location *)
         else (mt (), loc)
-      in pr_loc loc ++ hl
+      in Topfmt.pr_loc loc ++ hl
     ) loc
 
 (* Actual printing routine *)
@@ -185,12 +172,13 @@ let print_error_for_buffer ?loc lvl msg buf =
   then Topfmt.emacs_logger ?pre_hdr lvl msg
   else Topfmt.std_logger   ?pre_hdr lvl msg
 
+(*
 let print_toplevel_parse_error (e, info) buf =
   let loc = Loc.get_loc info in
   let lvl = Feedback.Error in
   let msg = CErrors.iprint (e, info) in
   print_error_for_buffer ?loc lvl msg buf
-
+*)
 end
 
 (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
@@ -272,7 +260,10 @@ let read_sentence sid input =
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
-    TopErr.print_toplevel_parse_error reraise top_buffer;
+    (* The caller of read_sentence does the error printing now, this
+       should be re-enabled once we rely on the feedback error
+       printer again *)
+    (* TopErr.print_toplevel_parse_error reraise top_buffer; *)
     Exninfo.iraise reraise
 
 (** Coqloop Console feedback handler *)
@@ -290,6 +281,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   | FileDependency (_,_) -> ()
   | FileLoaded (_,_) -> ()
   | Custom (_,_,_) -> ()
+  (* Re-enable when we switch back to feedback-based error printing *)
+  | Message (Error,loc,msg) -> ()
+  (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *)
   | Message (lvl,loc,msg) ->
     TopErr.print_error_for_buffer ?loc lvl msg top_buffer
 
@@ -309,18 +303,22 @@ let do_vernac sid =
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
-    Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input))
+    Vernac.process_expr sid (read_sentence sid (fst input))
   with
     | Stm.End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
     | CErrors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise CErrors.Drop
         else (Feedback.msg_error (str "There is no ML toplevel."); sid)
-    (* Exception printing is done now by the feedback listener. *)
-    (* XXX: We need this hack due to the side effects of the exception
-       printer and the reliance of Stm.define on attaching crutial
-       state to exceptions *)
-    | any -> ignore (CErrors.(iprint (push any))); sid
+    (* Exception printing should be done by the feedback listener,
+       however this is not yet ready so we rely on the exception for
+       now. *)
+    | any ->
+      let (e, info) = CErrors.push any in
+      let loc = Loc.get_loc info in
+      let msg = CErrors.iprint (e, info) in
+      TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+      sid
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 66bbf43f6..13e860a88 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-
 (** The Coq toplevel loop. *)
 
 (** A buffer for the character read from a channel. We store the command
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b7065993f..dc0c2beba 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -247,6 +247,7 @@ let set_emacs () =
   if not (Option.is_empty !toploop) then
     error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
+  Printer.enable_goal_tags_printing := true;
   color := `OFF
 
 (** Options for CoqIDE *)
@@ -291,9 +292,17 @@ let init_gc () =
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
 
+let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem"
+    (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
+
+exception NoCoqLib
 let usage () =
-  Envars.set_coqlib CErrors.error;
+  begin
+  try
+  Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib);
   init_load_path ();
+  with NoCoqLib -> usage_no_coqlib ()
+  end;
   if !batch_mode then Usage.print_usage_coqc ()
   else begin
     Mltop.load_ml_objects_raw_rex
@@ -430,10 +439,10 @@ let get_native_name s =
 
 (** Prints info which is either an error or an anomaly and then exits
     with the appropriate error code *)
-let fatal_error info anomaly =
-  let msg = info ++ fnl () in
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg;
-  exit (if anomaly then 129 else 1)
+let fatal_error ?extra exn =
+  Topfmt.print_err_exn ?extra exn;
+  let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
+  exit exit_code
 
 let parse_args arglist =
   let args = ref arglist in
@@ -596,11 +605,7 @@ let parse_args arglist =
   in
   try
     parse ()
-  with
-    | UserError(_, s) as e ->
-      if ismt s then exit 1
-      else fatal_error (CErrors.print e) false
-    | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any)
+  with any -> fatal_error any
 
 let init_toplevel arglist =
   init_gc ();
@@ -613,7 +618,7 @@ let init_toplevel arglist =
       (* If we have been spawned by the Spawn module, this has to be done
        * early since the master waits us to connect back *)
       Spawned.init_channels ();
-      Envars.set_coqlib CErrors.error;
+      Envars.set_coqlib ~fail:CErrors.error;
       if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
       if !print_config then (Usage.print_config (); exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
@@ -636,6 +641,9 @@ let init_toplevel arglist =
       init_library_roots ();
       load_vernac_obj ();
       require ();
+      (* XXX: This is incorrect in batch mode, as we will initialize
+         the STM before having done Declaremods.start_library, thus
+         state 1 is invalid. This bug was present in 8.5/8.6. *)
       Stm.init ();
       let sid  = load_rcfile (Stm.get_current_state ()) in
       (* XXX: We ignore this for now, but should be threaded to the toplevels *)
@@ -646,14 +654,13 @@ let init_toplevel arglist =
       check_vio_tasks ();
       outputstate ()
     with any ->
-      let any = CErrors.push any in
       flush_all();
-      let msg =
-        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then mt ()
-        else str "Error during initialization: " ++ CErrors.iprint any ++ fnl ()
+      let extra =
+        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
+        then None
+        else Some (str "Error during initialization: ")
       in
-      let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in
-      fatal_error msg (is_anomaly (fst any))
+      fatal_error ?extra any
   end;
   if !batch_mode then begin
     flush_all();
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 66f782ffb..e29048035 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -30,6 +30,7 @@ let print_usage_channel co command =
 \n  -R dir coqdir          recursively map physical dir to logical coqdir\
 \n  -Q dir coqdir          map physical dir to logical coqdir\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
+\n  -coqlib dir            set the coq standard library directory\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\
 \n  -noinit                start without loading the Init library\
@@ -83,7 +84,7 @@ let print_usage_channel co command =
 \n  -m, --memory           display total heap size at program exit\
 \n                         (use environment variable\
 \n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
-\n                          for full Gc stats dump)
+\n                          for full Gc stats dump)\
 \n  -native-compiler       precompile files for the native_compute machinery\
 \n  -h, -help, --help      print this list of options\
 \n";
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
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index e75f8f9e8..bbc095c68 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -8,11 +8,15 @@
 
 (** Parsing of vernacular. *)
 
-(** Reads and executes vernac commands from a stream. *)
-val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
+(** [process_expr sid cmd] Executes vernac command [cmd]. Callers are
+    expected to handle and print errors in form of exceptions, however
+    care is taken so the state machine is left in a consistent
+    state. *)
+val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
 
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
-    echo the commands if [echo] is set. *)
+    echo the commands if [echo] is set. Callers are expected to handle
+    and print errors in form of exceptions. *)
 val load_vernac : bool -> Stateid.t -> string -> Stateid.t
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)