More indirection.

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

4 files changed, 78 insertions, 79 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 2db5d81b9c..f385ae0489 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -83,17 +83,22 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
-let is_in_loadpath coqtop s = Ide_blob.eval_call (Ide_blob.is_in_loadpath s)
+let eval_call c =
+  match Ide_blob.eval_call c with
+    | Ide_blob.Good v -> v
+    | Ide_blob.Fail e -> raise e
+
+let is_in_loadpath coqtop s = eval_call (Ide_blob.is_in_loadpath s)
  
 let reset_initial = Ide_blob.reinit
 
-let raw_interp coqtop s = Ide_blob.eval_call (Ide_blob.raw_interp s)
+let raw_interp coqtop s = eval_call (Ide_blob.raw_interp s)
 
-let interp coqtop b s = Ide_blob.eval_call (Ide_blob.interp b s)
+let interp coqtop b s = eval_call (Ide_blob.interp b s)
 
-let rewind coqtop i = Ide_blob.eval_call (Ide_blob.rewind i)
+let rewind coqtop i = eval_call (Ide_blob.rewind i)
  
-let read_stdout coqtop = Ide_blob.eval_call Ide_blob.read_stdout
+let read_stdout coqtop = eval_call Ide_blob.read_stdout
 
 module PrintOpt =
 struct
@@ -160,8 +165,8 @@ type  tried_tactic =
 
 let goals coqtop =
   PrintOpt.enforce_hack ();
-  Ide_blob.eval_call Ide_blob.current_goals
+  eval_call Ide_blob.current_goals
 
-let make_cases coqtop s = Ide_blob.eval_call (Ide_blob.make_cases s)
+let make_cases coqtop s = eval_call (Ide_blob.make_cases s)
 
-let current_status coqtop = Ide_blob.eval_call Ide_blob.current_status
+let current_status coqtop = eval_call Ide_blob.current_status
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index 450a34282b..a312b0037b 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -275,7 +275,7 @@ let interp verbosely s =
     if is_vernac_known_option_command vernac then
       user_error_loc loc (str "Use CoqIDE display menu instead");
     if is_vernac_query_command vernac then
-      user_error_loc loc (str "Warning: query commands should not be inserted in scripts");
+      msgerrnl (str "Warning: query commands should not be inserted in scripts");
     if not (is_vernac_goal_printing_command vernac) then
       (* Verbose if in small step forward and not a tactic *)
       Flags.make_silent (not verbosely);
@@ -421,7 +421,6 @@ let current_goals () =
                    a ++ (Printer.pr_concl i sigma g) ++ (spc ())) 1
                 (str "This subproof is complete, but there are still unfocused goals:" ++ (fnl ()))
                 bgoals))
-
     end
   else
     begin
@@ -440,44 +439,6 @@ let current_goals () =
       Goals (List.map process_goal all_goals)
     end
 
-(*
-  let pfts = Proof_global.give_me_the_proof () in
-  let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals pfts in
-  if goals = [] then
-    begin
-      Message (string_of_ppcmds (
-        let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
-        match bgoals with
-          | [] ->
-              let exl = Evarutil.non_instantiated sigma in
-              (str (if exl = [] then "Proof Completed." else
-                      "No more subgoals but non-instantiated existential variables:") ++
-               (fnl ()) ++ (pr_evars_int 1 exl))
-          | _ ->
-              Util.list_fold_left_i
-                (fun i a g ->
-                   a ++ (Printer.pr_concl i sigma g) ++ (spc ())) 1
-                (str "This subproof is complete, but there are still unfocused goals:" ++ (fnl ()))
-                bgoals))
-    end
-  else
-    begin
-      let process_goal gs =
-        let (g,sigma) = Goal.V82.nf_evar sigma gs in
-        let env = Goal.V82.unfiltered_env sigma g in
-        let ccl =
-          string_of_ppcmds (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) in
-        let process_hyp h_env d acc =
-          (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in
-        let hyps =
-          List.rev (Environ.fold_named_context process_hyp env ~init:[]) in
-        (hyps,(ccl,concl_next_tac gs))
-      in
-      Goals (List.map process_goal all_goals)
-    end
- *)
-
-
 let id_of_name = function
   | Names.Anonymous -> id_of_string "x"
   | Names.Name x -> x
@@ -533,6 +494,24 @@ let init_stdout,read_stdout =
              let r = Buffer.contents out_buff in
              Buffer.clear out_buff; r)
 
+(* XXX - duplicates toplevel/toplevel.ml. should be merged. *)
+let explain_exn e =
+  let toploc,exc =
+    match e with
+      | Stdpp.Exc_located (loc, inner) ->
+          loc,inner
+      | Error_in_file (s, (is_in_lib, fname, loc), inner) ->
+          dummy_loc,inner
+      | _ -> dummy_loc,e
+  in
+  toploc,(Cerrors.explain_exn exc)
+
+
+(**
+ * Wrappers around Coq calls. We use phantom types and GADT to protect ourselves
+  * against wild casts
+  *)
+
 type 'a call =
   | In_loadpath of string
   | Raw_interp of string
@@ -543,17 +522,26 @@ type 'a call =
   | Cur_status
   | Cases of string
 
+type 'a value =
+  | Good of 'a
+  | Fail of exn
 
-let eval_call = function
-  | In_loadpath s -> Obj.magic (is_in_loadpath s)
-  | Raw_interp s -> Obj.magic (raw_interp s)
-  | Interp (b,s) -> Obj.magic (interp b s)
-  | Rewind i -> Obj.magic (rewind i)
-  | Read_stdout -> Obj.magic (read_stdout ())
-  | Cur_goals -> Obj.magic (current_goals ())
-  | Cur_status -> Obj.magic (current_status ())
-  | Cases s -> Obj.magic (make_cases s)
-
+let eval_call c = 
+  let filter_compat_exn = function
+    | Vernac.DuringCommandInterp (loc,inner)
+    | Vernacexpr.DuringSyntaxChecking (loc,inner) -> inner
+    | e -> e
+  in
+  try Good (match c with
+              | In_loadpath s -> Obj.magic (is_in_loadpath s)
+              | Raw_interp s -> Obj.magic (raw_interp s)
+              | Interp (b,s) -> Obj.magic (interp b s)
+              | Rewind i -> Obj.magic (rewind i)
+              | Read_stdout -> Obj.magic (read_stdout ())
+              | Cur_goals -> Obj.magic (current_goals ())
+              | Cur_status -> Obj.magic (current_status ())
+              | Cases s -> Obj.magic (make_cases s))
+  with e -> Fail (filter_compat_exn e)
 
 let is_in_loadpath s : bool call =
   In_loadpath s
@@ -578,3 +566,5 @@ let current_status : string call =
 
 let make_cases s : string list list call =
   Cases s
+
+(* End of wrappers *)
diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli
index 15fec45231..c74d67f2ce 100644
--- a/toplevel/ide_blob.mli
+++ b/toplevel/ide_blob.mli
@@ -21,7 +21,11 @@ val init_stdout : unit -> unit
 
 type 'a call
 
-val eval_call : 'a call -> 'a
+type 'a value =
+  | Good of 'a
+  | Fail of exn
+
+val eval_call : 'a call -> 'a value
 
 val raw_interp : string -> unit call
 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 6e679c7201..5e48a38aca 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -164,26 +164,26 @@ let print_location_in_file s inlibrary fname loc =
       hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++
              str"characters " ++ Cerrors.print_loc loc) ++ fnl ()
     else
-    let (bp,ep) = 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 (make_loc (bp-bol,ep-bol))) ++ str":" ++
-      fnl ()
-    with e ->
-      (close_in ic;
-       hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
+      let (bp,ep) = 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 (make_loc (bp-bol,ep-bol))) ++ str":" ++
+        fnl ()
+      with e ->
+        (close_in ic;
+         hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
 
 let print_command_location ib dloc =
   match dloc with