1 files changed, 140 insertions, 147 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7c4920df..bfdae85d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -9,27 +9,29 @@
 (* Parsing of vernacular. *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Flags
-open System
 open Vernacexpr
 
 (* The functions in this module may raise (unexplainable!) exceptions.
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-(* The navigation vernac commands will be handled separately *)
+let user_error loc s = CErrors.user_err_loc (loc,"_",str s)
+
+(* Navigation commands are allowed in a coqtop session but not in a .v file *)
 
 let rec is_navigation_vernac = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
-  | VernacBack _ -> true
-  | VernacRedirect (_, l) | VernacTime l ->
-    List.exists
-      (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
+  | VernacBack _
+  | VernacStm _ -> true
+  | VernacRedirect (_, (_,c))
+  | VernacTime (_,c) ->
+      is_navigation_vernac c (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
 
 and is_deep_navigation_vernac = function
@@ -42,6 +44,14 @@ let is_reset = function
   | VernacResetInitial | VernacResetName _ -> true
   | _ -> false
 
+let checknav_simple loc cmd =
+  if is_navigation_vernac cmd && not (is_reset cmd) then
+    user_error loc "Navigation commands forbidden in files."
+
+let checknav_deep loc ast =
+  if is_deep_navigation_vernac ast then
+    user_error loc "Navigation commands forbidden in nested commands."
+
 (* When doing Load on a file, two behaviors are possible:
 
    - either the history stack is grown by only one command,
@@ -66,32 +76,10 @@ let _ =
       Goptions.optread  = (fun () -> !atomic_load);
       Goptions.optwrite = ((:=) atomic_load) }
 
-(* In case of error, register the file being currently Load'ed and the
-   inner file in which the error has been encountered. Any intermediate files
-   between the two are discarded. *)
-
-type location_files = { outer : string; inner : string }
-
-let files_of_exn : location_files Exninfo.t = Exninfo.make ()
-
-let get_exn_files e = Exninfo.get e files_of_exn
-
-let add_exn_files e f = Exninfo.add e files_of_exn f
-
-let enrich_with_file f (e, info) =
-  let inner = match get_exn_files info with None -> f | Some x -> x.inner in
-  (e, add_exn_files info { outer = f; inner })
-
-let raise_with_file f e = iraise (enrich_with_file f e)
-
-let cur_file = ref None
-
 let disable_drop = function
-  | Drop -> Errors.error "Drop is forbidden."
+  | Drop -> CErrors.error "Drop is forbidden."
   | e -> e
 
-let user_error loc s = Errors.user_err_loc (loc,"_",str s)
-
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
    Note: we could use only one thanks to seek_in, but seeking on and on in
@@ -101,7 +89,7 @@ let open_file_twice_if verbosely longfname =
   let in_chan = open_utf8_file_in longfname in
   let verb_ch =
     if verbosely then Some (open_utf8_file_in longfname) else None in
-  let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
+  let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
   (in_chan, longfname, (po, verb_ch))
 
 let close_input in_chan (_,verb) =
@@ -110,7 +98,7 @@ let close_input in_chan (_,verb) =
     match verb with
       | Some verb_ch -> close_in verb_ch
       | _ -> ()
-  with e when Errors.noncritical e -> ()
+  with e when CErrors.noncritical e -> ()
 
 let verbose_phrase verbch loc =
   let loc = Loc.unloc loc in
@@ -120,8 +108,7 @@ let verbose_phrase verbch loc =
 	let s = String.create len in
         seek_in ch (fst loc);
         really_input ch s 0 len;
-        ppnl (str s);
-        pp_flush()
+        Feedback.msg_notice (str s)
     | None -> ()
 
 exception End_of_input
@@ -135,51 +122,44 @@ let parse_sentence = Flags.with_option Flags.we_are_parsing
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
 
-let just_parsing = ref false
 let chan_beautify = ref stdout
 let beautify_suffix = ".beautified"
 
-let set_formatter_translator() =
-  let ch = !chan_beautify in
+let set_formatter_translator ch =
   let out s b e = output ch s b e in
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
-let pr_new_syntax loc ocom =
+let pr_new_syntax_in_context loc chan_beautify ocom =
   let loc = Loc.unloc loc in
-  if !beautify_file then set_formatter_translator();
+  if !beautify_file then set_formatter_translator chan_beautify;
   let fs = States.freeze ~marshallable:`No in
-  let com = match ocom with
-    | Some VernacNop -> mt()
-    | Some com -> Ppvernac.pr_vernac com
-    | None -> mt() in
-  if !beautify_file then
-    msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
-  else
-    msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
-  States.unfreeze fs;
-  Format.set_formatter_out_channel stdout
-
-let save_translator_coqdoc () =
-  (* translator state *)
-  let ch = !chan_beautify in
-  let cl = !Pp.comments in
-  let cs = Lexer.com_state() in
-  (* end translator state *)
-  let coqdocstate = Lexer.location_table () in
-  ch,cl,cs,coqdocstate
-
-let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
-  if !Flags.beautify_file then close_out !chan_beautify;
-  chan_beautify := ch;
-  Pp.comments := cl;
-  Lexer.restore_com_state cs;
-  Lexer.restore_location_table coqdocstate
+  (* The content of this is not supposed to fail, but if ever *)
+  try
+    (* Side-effect: order matters *)
+    let before = comment (CLexer.extract_comments (fst loc)) in
+    let com = match ocom with
+      | Some com -> Ppvernac.pr_vernac com
+      | None -> mt() in
+    let after = comment (CLexer.extract_comments (snd loc)) in
+    if !beautify_file then
+      Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
+    else
+      Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+    States.unfreeze fs;
+    Format.set_formatter_out_channel stdout
+  with any ->
+    States.unfreeze fs;
+    Format.set_formatter_out_channel stdout
+
+let pr_new_syntax po loc chan_beautify ocom =
+  (* Reinstall the context of parsing which includes the bindings of comments to locations *)
+  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context chan_beautify loc) ocom
 
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
 
-let display_cmd_header loc com =
+let pp_cmd_header loc com =
   let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
   let noblank s =
     for i = 0 to String.length s - 1 do
@@ -194,75 +174,63 @@ let display_cmd_header loc com =
     try Ppvernac.pr_vernac x
     with e -> str (Printexc.to_string e) in
   let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
-  in
-  Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
-	 str " [" ++ str cmd ++ str "] ");
-  Pp.flush_all ()
+  in str "Chars " ++ int start ++ str " - " ++ int stop ++
+     str " [" ++ str cmd ++ str "] "
 
-let rec vernac_com verbose checknav (loc,com) =
+(* This is a special case where we assume we are in console batch mode
+   and take control of the console.
+ *)
+let print_cmd_header loc com =
+  Pp.pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (pp_cmd_header loc com);
+  Format.pp_print_flush !Pp_control.std_ft ()
+
+let rec interp_vernac po chan_beautify checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
-	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
-	let st = save_translator_coqdoc () in
-	if !Flags.beautify_file then
-	  begin
-	    chan_beautify := open_out (f^beautify_suffix);
-	    Pp.comments := []
-          end;
-	begin
-	  try
-            read_vernac_file verbosely f;
-	    restore_translator_coqdoc st;
-	  with reraise ->
-            let reraise = Errors.push reraise in
-	    restore_translator_coqdoc st;
-	    iraise reraise
-	end
-
-    | v when !just_parsing -> ()
-
-    | v -> Stm.interp verbose (loc,v)
+        load_vernac verbosely f
+
+    | v -> Stm.interp (Flags.is_verbose()) (loc,v)
   in
     try
       checknav loc com;
-      if do_beautify () then pr_new_syntax loc (Some com);
-      if !Flags.time then display_cmd_header loc com;
-      let com = if !Flags.time then VernacTime [loc,com] else com in
+      if !beautify then pr_new_syntax po chan_beautify loc (Some com);
+      (* XXX: This is not 100% correct if called from an IDE context *)
+      if !Flags.time then print_cmd_header loc com;
+      let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
     with reraise ->
-      let (reraise, info) = Errors.push reraise in
-      Format.set_formatter_out_channel stdout;
+      let (reraise, info) = CErrors.push reraise in
       let loc' = Option.default Loc.ghost (Loc.get_loc info) in
       if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
       else iraise (reraise, info)
 
-and read_vernac_file verbosely s =
-  let checknav loc cmd =
-    if is_navigation_vernac cmd && not (is_reset cmd) then
-	user_error loc "Navigation commands forbidden in files"
-  in
-  let (in_chan, fname, input) = open_file_twice_if verbosely s in
-  cur_file := Some fname;
+(* Load a vernac file. CErrors are annotated with file and location *)
+and load_vernac verbosely file =
+  let chan_beautify =
+    if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in
+  let (in_chan, fname, input) = open_file_twice_if verbosely file 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 verbosely checknav loc_ast;
-      pp_flush ()
+      let loc_ast = Flags.silently parse_sentence input in
+      CWarnings.set_current_loc (fst loc_ast);
+      Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast;
     done
   with any ->   (* whatever the exception *)
-    let (e, info) = Errors.push any in
-    Format.set_formatter_out_channel stdout;
+    let (e, info) = CErrors.push any in
     close_input in_chan input;    (* we must close the file first *)
     match e with
       | End_of_input ->
-          cur_file := None;
-          if do_beautify () then
-            pr_new_syntax (Loc.make_loc (max_int,max_int)) None
-      | _ -> raise_with_file fname (disable_drop e, info)
+          if !beautify then
+            pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None;
+          if !Flags.beautify_file then close_out chan_beautify;
+      | reraise ->
+         if !Flags.beautify_file then close_out chan_beautify;
+	 iraise (disable_drop e, info)
 
 (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
    It executes one vernacular command. By default the command is
@@ -271,34 +239,50 @@ and read_vernac_file verbosely s =
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-let checknav loc ast =
-  if is_deep_navigation_vernac ast then
-    user_error loc "Navigation commands forbidden in nested commands"
-
-let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
+let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
 let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
 
-(* Load a vernac file. Errors are annotated with file and location *)
-let load_vernac verb file =
-  chan_beautify :=
-    if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
-  try
-    Flags.silently (read_vernac_file verb) file;
-    if !Flags.beautify_file then close_out !chan_beautify;
-  with any ->
-    let (e, info) = Errors.push any in
-    if !Flags.beautify_file then close_out !chan_beautify;
-    raise_with_file file (disable_drop e, info)
+let warn_file_no_extension =
+  CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
+         (fun (f,ext) ->
+          str "File \"" ++ str f ++
+            strbrk "\" has been implicitly expanded to \"" ++
+            str f ++ str ext ++ str "\"")
 
-let ensure_v f =
-  if Filename.check_suffix f ".v" then f
+let ensure_ext ext f =
+  if Filename.check_suffix f ext then f
   else begin
-    msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
-    expanded to \"" ++ str f ++ str ".v\"");
-    f ^ ".v"
+    warn_file_no_extension (f,ext);
+    f ^ ext
+  end
+
+let chop_extension f =
+  try Filename.chop_extension f with _ -> 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");
+    Feedback.msg_error (str "Source: " ++ str src);
+    Feedback.msg_error (str "Target: " ++ str tgt);
+    flush_all ();
+    exit 1
+  end
+
+let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
+
+let ensure_v v = ensure ".v" v v
+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
 
 (* Compile a vernac file *)
@@ -306,14 +290,21 @@ let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
     if not (List.is_empty pfs) then
-      (msg_error (str "There are pending proofs"); flush_all (); exit 1) in
+      (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in
   match !Flags.compilation_mode with
   | BuildVo ->
       let long_f_dot_v = ensure_v f in
-      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
-      Stm.set_compilation_hints long_f_dot_v;
-      Aux_file.start_aux_file_for long_f_dot_v;
-      Dumpglob.start_dump_glob long_f_dot_v;
+      ensure_exists long_f_dot_v;
+      let long_f_dot_vo =
+        match !Flags.compilation_output_name with
+        | None -> long_f_dot_v ^ "o"
+        | Some f -> ensure_vo long_f_dot_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_vo in
+      Stm.set_compilation_hints long_f_dot_vo;
+      Aux_file.(start_aux_file
+        ~aux_file:(aux_file_name_for long_f_dot_vo)
+        ~v_file:long_f_dot_v);
+      Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       if !Flags.xml_export then Hook.get f_xml_start_library ();
       let wall_clock1 = Unix.gettimeofday () in
@@ -321,7 +312,7 @@ let compile verbosely f =
       Stm.join ();
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
-      Library.save_library_to ldir long_f_dot_v (Global.opaque_tables ());
+      Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
       Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
@@ -329,13 +320,18 @@ let compile verbosely f =
       Dumpglob.end_dump_glob ()
   | BuildVio ->
       let long_f_dot_v = ensure_v f in
-      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
+      ensure_exists long_f_dot_v;
+      let long_f_dot_vio =
+        match !Flags.compilation_output_name with
+        | None -> long_f_dot_v ^ "io"
+        | Some f -> ensure_vio long_f_dot_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_vio in
       Dumpglob.noglob ();
-      Stm.set_compilation_hints long_f_dot_v;
+      Stm.set_compilation_hints long_f_dot_vio;
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
-      Stm.snapshot_vio ldir long_f_dot_v;
+      Stm.snapshot_vio ldir long_f_dot_vio;
       Stm.reset_task_queue ()
   | Vio2Vo ->
       let open Filename in
@@ -352,8 +348,5 @@ let compile v f =
   compile v f;
   CoqworkmgrApi.giveback 1
 
-let () = Hook.set Stm.process_error_hook (fun e ->
-  match !cur_file with
-  | None -> Cerrors.process_vernac_interp_error e
-  | Some f -> enrich_with_file f (Cerrors.process_vernac_interp_error e)
-)
+let () = Hook.set Stm.process_error_hook
+  ExplainErr.process_vernac_interp_error