diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 49 |
1 files changed, 25 insertions, 24 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index eb97755fa..222b9eed9 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -366,6 +366,9 @@ object(self) (* This method is intended to perform stateless commands *) method raw_coq_query phrase = + let sid = try Document.tip document + with Document.Empty -> Stateid.initial + in let action = log "raw_coq_query starting now" in let display_error s = if not (validate s) then @@ -373,11 +376,10 @@ object(self) else messages#add s; in let query = - Coq.query (phrase,Stateid.dummy) in + Coq.query (phrase,sid) in let next = function | Fail (_, _, err) -> display_error err; Coq.return () - | Good msg -> - messages#add_string msg; Coq.return () + | Good msg -> Coq.return () in Coq.bind (Coq.seq action query) next @@ -414,12 +416,9 @@ object(self) buffer#apply_tag Tags.Script.tooltip ~start ~stop; add_tooltip sentence pre post markup - method private is_dummy_id id = Stateid.equal id Stateid.dummy - method private enqueue_feedback msg = - (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *) - let id = msg.id in - if self#is_dummy_id id then () else Queue.add msg feedbacks + (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt Xmlprotocol.(of_feedback Ppcmds msg)); *) + Queue.add msg feedbacks method private process_feedback () = let rec eat_feedback n = @@ -433,41 +432,41 @@ object(self) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in - let log_pp s state_id = + let log_pp ?id s= Minilib.log_pp Pp.(seq - [str "Feedback "; s; str " on "; - str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in - let log s state_id = log_pp (Pp.str s) state_id in + [str "Feedback "; s; pr_opt (fun id -> str " on " ++ str (Stateid.to_string id)) id]) + in + let log ?id s = log_pp ?id (Pp.str s) in begin match msg.contents, sentence with | AddedAxiom, Some (id,sentence) -> - log "AddedAxiom" id; + log ?id "AddedAxiom"; remove_flag sentence `PROCESSING; remove_flag sentence `ERROR; add_flag sentence `UNSAFE; self#mark_as_needed sentence | Processed, Some (id,sentence) -> - log "Processed" id; + log ?id "Processed" ; remove_flag sentence `PROCESSING; self#mark_as_needed sentence | ProcessingIn _, Some (id,sentence) -> - log "ProcessingIn" id; + log ?id "ProcessingIn"; add_flag sentence `PROCESSING; self#mark_as_needed sentence | Incomplete, Some (id, sentence) -> - log "Incomplete" id; + log ?id "Incomplete"; add_flag sentence `INCOMPLETE; self#mark_as_needed sentence | Complete, Some (id, sentence) -> - log "Complete" id; + log ?id "Complete"; remove_flag sentence `INCOMPLETE; self#mark_as_needed sentence | GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) -> - log "GlobRef" id; + log ?id "GlobRef"; self#attach_tooltip ~loc sentence (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> let uloc = Option.default Loc.ghost loc in - log_pp Pp.(str "ErrorMsg" ++ msg) id; + log_pp ?id Pp.(str "ErrorMsg" ++ msg); remove_flag sentence `PROCESSING; let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`ERROR (uloc, rmsg)); @@ -476,22 +475,24 @@ object(self) self#position_tag_at_sentence ?loc Tags.Script.error sentence | Message(Warning, loc, msg), Some (id,sentence) -> let uloc = Option.default Loc.ghost loc in - log_pp Pp.(str "WarningMsg" ++ msg) id; + log_pp ?id Pp.(str "WarningMsg" ++ msg); let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`WARNING (uloc, rmsg)); self#attach_tooltip sentence ?loc rmsg; self#position_tag_at_sentence ?loc Tags.Script.warning sentence; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - log_pp Pp.(str "Msg" ++ msg) id; + log_pp ?id Pp.(str "Msg" ++ msg); + messages#push lvl msg + | Message(lvl, loc, msg), None -> + log_pp Pp.(str "Msg" ++ msg); messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n | WorkerStatus(id,status), _ -> - log "WorkerStatus" None; + log "WorkerStatus"; slaves_status <- CString.Map.add id status slaves_status - | _ -> if sentence <> None then Minilib.log "Unsupported feedback message" else if Doc.is_empty document then () @@ -500,7 +501,7 @@ object(self) match id, Doc.tip document with | id1, id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks - with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks + with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks end; eat_feedback (n-1) in |