diff options
| author |  vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-07 10:40:40 +0000 |
|---|---|---|
| committer | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-07 10:40:40 +0000 |
| commit | 33c86e54a60a79a59b30fe925f2cd4b147048eae (patch) | |
| tree | ada86869cddf93fc190848335dab65b1e1af8e51 /toplevel | |
| parent | 1386cd9f79aa40e84757ae9eddced66cc48f9c1c (diff) | |
fixing error message display.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13082 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ide_blob.ml | 11 | ||||
| -rw-r--r-- | toplevel/ide_blob.mli | 2 |
2 files changed, 6 insertions, 7 deletions
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index 81ad61930..b4173f0ca 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -502,10 +502,10 @@ let explain_exn e = let toploc,exc = match e with | Loc.Exc_located (loc, inner) -> - loc,inner + (if loc = dummy_loc then None else Some loc),inner | Error_in_file (s, (is_in_lib, fname, loc), inner) -> - dummy_loc,inner - | _ -> dummy_loc,e + None,inner + | _ -> None,e in toploc,(Cerrors.explain_exn exc) @@ -527,7 +527,7 @@ type 'a call = type 'a value = | Good of 'a - | Fail of (Util.loc * Pp.std_ppcmds) + | Fail of (Util.loc option * string) let eval_call c = let null_formatter = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in @@ -549,8 +549,7 @@ let eval_call c = with e -> let (l,pp) = explain_exn (filter_compat_exn e) in (* force evaluation of format stream *) - Pp.msg_with null_formatter pp; - Fail (l,pp) + Fail (l,string_of_ppcmds pp) let is_in_loadpath s : bool call = In_loadpath s diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli index 561821b56..7a34680d1 100644 --- a/toplevel/ide_blob.mli +++ b/toplevel/ide_blob.mli @@ -23,7 +23,7 @@ type 'a call type 'a value = | Good of 'a - | Fail of (Util.loc * Pp.std_ppcmds) + | Fail of (Util.loc option * string) val eval_call : 'a call -> 'a value |