diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-25 17:35:36 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-25 17:35:36 +0000 |
| commit | bac77d6d0e58c74e2ad8ca439c48b86df5587206 (patch) | |
| tree | 30e1111ced9c70138ef9544ae2a0af8de8dc6407 /ide/coqide.ml | |
| parent | 0e11499aefb286877fd3cd41e05d23f120a55cc7 (diff) | |
Ide_intf : change type of location in ide
We use (int * int) option instead of Loc.t, it's easier to use
later in coqide, and this way we do not depend on camlp4,5
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13929 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 1797a7e51..e553ca0b4 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -803,7 +803,7 @@ object(self) method send_to_coq verbosely replace phrase show_output show_error localize = let display_output msg = self#insert_message (if show_output then msg else "") in - let display_error (s,loc) = + let display_error (loc,s) = if show_error then begin if not (Glib.Utf8.validate s) then flash_info "This error is so nasty that I can't even display it." @@ -811,7 +811,7 @@ object(self) self#insert_message s; message_view#misc#draw None; if localize then - (match Option.map Util.unloc loc with + (match loc with | None -> () | Some (start,stop) -> let convert_pos = byte_offset_to_char_offset phrase in @@ -830,7 +830,7 @@ object(self) full_goal_done <- false; prerr_endline "Send_to_coq starting now"; match Coq.interp mycoqtop verbosely phrase with - | Ide_intf.Fail (l,str) -> sync display_error (str,l); None + | Ide_intf.Fail (l,str) -> sync display_error (l,str); None | Ide_intf.Good r -> match Coq.read_stdout mycoqtop with | Ide_intf.Fail (_,str) -> |