diff options
Diffstat (limited to 'ide/coqOps.ml')
| -rw-r--r-- | ide/coqOps.ml | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 7825fb45e..50d0dc491 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -14,7 +14,7 @@ open Feedback let b2c = byte_offset_to_char_offset -type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ] +type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string Loc.located | `WARNING of string Loc.located ] type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ] let mem_flag_of_flag : flag -> mem_flag = function | `ERROR _ -> `ERROR @@ -467,19 +467,15 @@ object(self) | Message(Error, loc, msg), Some (id,sentence) -> log_pp ?id Pp.(str "ErrorMsg" ++ msg); remove_flag sentence `PROCESSING; - let rmsg = Pp.string_of_ppcmds msg in - Option.iter (fun loc -> - add_flag sentence (`ERROR (loc, rmsg)); - ) loc; + let rmsg = Pp.string_of_ppcmds msg in + add_flag sentence (`ERROR (loc, rmsg)); self#mark_as_needed sentence; self#attach_tooltip ?loc sentence rmsg; self#position_tag_at_sentence ?loc Tags.Script.error sentence | Message(Warning, loc, msg), Some (id,sentence) -> log_pp ?id Pp.(str "WarningMsg" ++ msg); let rmsg = Pp.string_of_ppcmds msg in - Option.iter (fun loc -> - add_flag sentence (`WARNING (loc, rmsg)); - ) loc; + add_flag sentence (`WARNING (loc, rmsg)); self#attach_tooltip ?loc sentence rmsg; self#position_tag_at_sentence ?loc Tags.Script.warning sentence; messages#push Warning msg @@ -683,14 +679,13 @@ object(self) let extract_error s = match List.find (function `ERROR _ -> true | _ -> false) s.flags with | `ERROR (loc, msg) -> - let iter = - if Loc.is_ghost loc then - buffer#get_iter_at_mark s.start - else + let iter = begin match loc with + | None -> buffer#get_iter_at_mark s.start + | Some loc -> let (iter, _, phrase) = self#get_sentence s in let (start, _) = Loc.unloc loc in - iter#forward_chars (b2c phrase start) in - iter#line + 1, msg + iter#forward_chars (b2c phrase start) + end in iter#line + 1, msg | _ -> assert false in List.rev (Doc.fold_all document [] (fun acc _ _ s -> |