aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-19 19:55:17 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-19 23:06:25 +0200
commitb3ed40b82540639de925afd36a32fbd716d2800f (patch)
tree5c395650ce4495e4e4e6442cc5fd8a57ed4be60a /ide
parentbeb3acd2fd3831404f0be2da61d3f28e210e8349 (diff)
[ide] Rely less on `Stateid.dummy`
In particular, we set queries from the menu to the tip of the document, and process feedback coming with a `dummy` id. There are still more places to tweak, but this should be good for now. We also display a few more query messages, in particular the feedbacks produced by query that carry a dummy state id. This hack of reporting with from the STM should be solved once we update the protocol.
Diffstat (limited to 'ide')
-rw-r--r--ide/coqOps.ml49
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