Vernac+Toplevel: get rid of Error_in_file

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

8 files changed, 77 insertions, 99 deletions

diff --git a/lib/errors.ml b/lib/errors.ml
index 0d13fcd2f9..75464f2da0 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -47,11 +47,6 @@ let todo s = prerr_string ("TODO: "^s^"\n")
 let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
 
-(* Like Exc_located, but specifies the outermost file read, the filename
-   associated to the location of the error, and the error itself. *)
-
-exception Error_in_file of string * (bool * string * Loc.t) * exn
-
 exception Timeout
 exception Drop
 exception Quit
diff --git a/lib/errors.mli b/lib/errors.mli
index 5f230d4c3b..c5400574b8 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -51,12 +51,6 @@ exception Timeout
 exception Drop
 exception Quit
 
-(** Like [Exc_located], but specifies the outermost file read, the
-   input buffer associated to the location of the error (or the module name
-   if boolean is true), and the error itself. *)
-
-exception Error_in_file of string * (bool * string * Loc.t) * exn
-
 (** [register_handler h] registers [h] as a handler.
     When an expression is printed with [print e], it
     goes through all registered handles (the most
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 7758daf652..ce74b361de 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -285,20 +285,17 @@ let quit = ref false
 (** Grouping all call handlers together + error handling *)
 
 let eval_call c =
-  let rec handle_exn e =
+  let handle_exn e =
     catch_break := false;
-    let pr_exn e = (read_stdout ())^("\n"^(string_of_ppcmds (Errors.print e))) in
     match e with
       | Errors.Drop -> None, "Drop is not allowed by coqide!"
       | Errors.Quit -> None, "Quit is not allowed by coqide!"
-      | Error_in_file (_,_,inner) -> None, pr_exn inner
       | e ->
         let loc = match Loc.get_loc e with
-        | None -> None
-        | Some loc ->
-          if Loc.is_ghost loc then None else Some (Loc.unloc loc)
+          | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
+          | _ -> None
         in
-        loc, pr_exn e
+        loc, (read_stdout ())^"\n"^(string_of_ppcmds (Errors.print e))
   in
   let interruptible f x =
     catch_break := true;
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 6947d95e76..1a318e5e18 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -150,37 +150,34 @@ let print_highlight_location ib loc =
 
 (* Functions to report located errors in a file. *)
 
-let print_location_in_file s inlibrary fname loc =
+let print_location_in_file {outer=s;inner=fname} loc =
   let errstrm = str"Error while reading " ++ str s in
   if Loc.is_ghost loc then
     hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
   else
     let errstrm =
-      if String.equal s fname then mt() else errstrm ++ str":" ++ fnl() in
-    if inlibrary then
-      hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++
-             str"characters " ++ Cerrors.print_loc loc) ++ fnl ()
-    else
-      let (bp,ep) = Loc.unloc loc in
-      let ic = open_in fname in
-      let rec line_of_pos lin bol cnt =
-        if cnt < bp then
-          if input_char ic == '\n'
-          then line_of_pos (lin + 1) (cnt +1) (cnt+1)
-          else line_of_pos lin bol (cnt+1)
-        else (lin, bol)
-      in
-      try
-        let (line, bol) = line_of_pos 1 0 0 in
-        close_in ic;
-        hov 0 (* No line break so as to follow emacs error message format *)
-          (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
+      if String.equal s fname then mt() else errstrm ++ str":" ++ fnl()
+    in
+    let (bp,ep) = Loc.unloc loc in
+    let ic = open_in fname in
+    let rec line_of_pos lin bol cnt =
+      if cnt < bp then
+        if input_char ic == '\n'
+        then line_of_pos (lin + 1) (cnt +1) (cnt+1)
+        else line_of_pos lin bol (cnt+1)
+      else (lin, bol)
+    in
+    try
+      let (line, bol) = line_of_pos 1 0 0 in
+      close_in ic;
+      hov 0 (* No line break so as to follow emacs error message format *)
+        (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
            str", line " ++ int line ++ str", characters " ++
            Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++
         fnl ()
-      with e when Errors.noncritical e ->
-        (close_in ic;
-         hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
+    with e when Errors.noncritical e ->
+      (close_in ic;
+       hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
 
 let valid_buffer_loc ib loc =
   not (Loc.is_ghost loc) &&
@@ -251,25 +248,24 @@ let set_prompt prompt =
     ^ prompt ()
     ^ emacs_prompt_endstring())
 
-(* Removes and prints the location of the error. The following exceptions
-   need not be located. *)
-let rec is_pervasive_exn = function
-  | Out_of_memory | Stack_overflow | Sys.Break -> true
-  | Error_in_file (_,_,e) -> is_pervasive_exn e
-  | _ -> false
-
-(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
-   May raise only the following exceptions: Drop and End_of_input,
-   meaning we get out of the Coq loop *)
-let print_toplevel_error = function
-  | Error_in_file (s, (inlibrary, fname, loc), e) ->
-      print_location_in_file s inlibrary fname loc ++ Errors.print e
-  | e ->
-      if is_pervasive_exn e then Errors.print e
-      else match Loc.get_loc e with
-        | Some loc when valid_buffer_loc top_buffer loc ->
-          print_highlight_location top_buffer loc ++ Errors.print e
-        | _ -> Errors.print e
+(* The following exceptions need not be located. *)
+
+let rec locate_exn = function
+  | Out_of_memory | Stack_overflow | Sys.Break -> false
+  | _ -> true
+
+(* Toplevel error explanation. *)
+
+let print_toplevel_error e =
+  let loc = Option.default Loc.ghost (Loc.get_loc e) in
+  let locmsg = match Vernac.get_exn_files e with
+    | Some files -> print_location_in_file files loc
+    | None ->
+      if locate_exn e && valid_buffer_loc top_buffer loc then
+        print_highlight_location top_buffer loc
+      else mt ()
+  in
+  locmsg ++ Errors.print e
 
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a2563a6761..f46ef8f130 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -94,24 +94,24 @@ let _ =
       Goptions.optread  = (fun () -> !atomic_load);
       Goptions.optwrite = ((:=) atomic_load) }
 
-(* Specifies which file is read. The intermediate file names are
-   discarded here. The Drop exception becomes an error. We forget
-   if the error ocurred during interpretation or not *)
-
-let raise_with_file file exc =
-  let (inner,inex) =
-    match exc with
-      | Error_in_file (_, (b,f,loc), e) when not (Loc.is_ghost loc) ->
-          ((b, f, loc), e)
-      | e ->
-        match Loc.get_loc e with
-        | Some loc when not (Loc.is_ghost loc) -> ((false,file,loc), e)
-        | _ -> ((false,file,Loc.ghost), e)
-  in
-  raise (Error_in_file (file, inner, disable_drop inex))
+(* 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 real_error = function
-  | Error_in_file (_, _, e) -> e
+let add_exn_files e f = Exninfo.add e files_of_exn f
+
+let raise_with_file f e =
+  let inner_f = match get_exn_files e with None -> f | Some ff -> ff.inner in
+  raise (add_exn_files e { outer = f; inner = inner_f })
+
+let disable_drop = function
+  | Drop -> Errors.error "Drop is forbidden."
   | e -> e
 
 let user_error loc s = Errors.user_err_loc (loc,"_",str s)
@@ -292,22 +292,20 @@ let rec vernac_com interpfun checknav (loc,com) =
     | v when !just_parsing -> true
 
     | VernacFail v ->
-	begin try
+      begin
+        try
 	  (* If the command actually works, ignore its effects on the state *)
 	  States.with_state_protection
 	    (fun v -> ignore (interp v); raise HasNotFailed) v
-	with e when Errors.noncritical e ->
-          let e = Errors.push e in
-          match real_error e with
-	  | HasNotFailed ->
-	      errorlabstrm "Fail" (str "The command has not failed !")
-	  | e ->
-              (* NB: e here cannot be an anomaly *)
+        with
+          | HasNotFailed ->
+              errorlabstrm "Fail" (str "The command has not failed !")
+          | e when Errors.noncritical e -> (* In particular e is no anomaly *)
 	      if_verbose msg_info
 		(str "The command has indeed failed with message:" ++
 		 fnl () ++ str "=> " ++ hov 0 (Errors.print e));
               true
-	end
+      end
 
     | VernacTime v ->
 	  let tstart = System.get_time() in
@@ -378,17 +376,15 @@ and read_vernac_file verbosely s =
       pp_flush ()
     done;
     assert false
-  with e ->   (* whatever the exception *)
-    (* TODO: restrict to Errors.noncritical or not ?
-       Morally, this is a reraise ... *)
-    let e = Errors.push e in
+  with any ->   (* whatever the exception *)
+    let e = Errors.push any in
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
-    match real_error e with
+    match e with
       | End_of_input ->
           if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None;
           !status
-      | _ -> raise_with_file fname e
+      | _ -> raise_with_file fname (disable_drop e)
 
 (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
    It executes one vernacular command. By default the command is
@@ -425,7 +421,7 @@ let load_vernac verb file =
   with any ->
     let e = Errors.push any in
     if !Flags.beautify_file then close_out !chan_beautify;
-    raise_with_file file e
+    raise_with_file file (disable_drop e)
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index e0ca6db468..9ef3bc28a9 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -49,3 +49,9 @@ val is_navigation_vernac : Vernacexpr.vernac_expr -> bool
 
 (** Should we display timings for each command ? *)
 val time : bool ref
+
+(** Has an exception been annotated with some file locations ? *)
+
+type location_files = { outer : string; inner : string }
+
+val get_exn_files : exn -> location_files option
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 9c5db8fd95..e15edf4e9a 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -9,10 +9,6 @@
 open Pp
 open Errors
 
-let disable_drop e =
-  if e <> Drop then e
-  else UserError("Vernac.disable_drop",(str"Drop is forbidden."))
-
 (* Table of vernac entries *)
 let vernac_tab =
   (Hashtbl.create 51 :
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index efe7e073ed..7138c36f1e 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -10,8 +10,6 @@ open Tacexpr
 
 (** Interpretation of extended vernac phrases. *)
 
-val disable_drop : exn -> exn
-
 val vinterp_add : string -> (raw_generic_argument list -> unit -> unit) -> unit
 val overwriting_vinterp_add :
   string -> (raw_generic_argument list -> unit -> unit) -> unit