From b3ed40b82540639de925afd36a32fbd716d2800f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 19 Apr 2017 19:55:17 +0200 Subject: [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. --- ide/coqOps.ml | 49 +++++++++++++++++++++++++------------------------ 1 file changed, 25 insertions(+), 24 deletions(-) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index eb97755fa6..222b9eed9f 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 -- cgit v1.2.3 From 61b946cde62d3324c39f663974d4cfadd9207a69 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 19 Apr 2017 23:24:41 +0200 Subject: [ide] Set Stateid in query pane. We again remove another user of Stateid.dummy. However, we need to adapt the protocol so `Coq.query` takes the `route_id` and we can redirect the output properly to the subwindow. --- ide/session.ml | 2 +- ide/wg_Command.ml | 13 +++++++++++-- ide/wg_Command.mli | 2 +- 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/ide/session.ml b/ide/session.ml index fc6340d283..6262820e7b 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -386,12 +386,12 @@ let create file coqtop_args = let proof = create_proof () in let messages = create_messages () in let segment = new Wg_Segment.segment () in - let command = new Wg_Command.command_window basename coqtop in let finder = new Wg_Find.finder basename (script :> GText.view) in let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in let _ = fops#update_stats in let cops = new CoqOps.coqops script proof messages segment coqtop (fun () -> fops#filename) in + let command = new Wg_Command.command_window basename coqtop cops in let errpage = create_errpage script in let jobpage = create_jobpage coqtop cops in let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 47dad8f196..3fcb7ce49e 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -8,7 +8,7 @@ open Preferences -class command_window name coqtop = +class command_window name coqtop coqops = let frame = Wg_Detachable.detachable ~title:(Printf.sprintf "Query pane (%s)" name) () in let _ = frame#hide in @@ -26,6 +26,11 @@ object(self) val notebook = notebook + (* We need access to coqops in order to place queries in the proper + document stint. This should remove access from this module to the + low-level Coq one. *) + val coqops = coqops + method pack_in (f : GObj.widget -> unit) = f frame#coerce val mutable new_page : GObj.widget = (GMisc.label ())#coerce @@ -101,7 +106,10 @@ object(self) else com ^ " " ^ arg ^" . " in let process = - Coq.bind (Coq.query (phrase,Stateid.dummy)) (function + (* We need to adapt this to route_id and redirect to the result buffer below *) + coqops#raw_coq_query phrase + (* + Coq.bind (Coq.query (phrase,sid)) (function | Interface.Fail (_,l,str) -> let width = Ideutils.textview_width result in Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str); @@ -111,6 +119,7 @@ object(self) result#buffer#insert res; notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce; Coq.return ()) + *) in result#buffer#set_text ("Result for command " ^ phrase ^ ":\n"); Coq.try_grab coqtop process ignore diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli index fa50ba5fdd..341322be1b 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -class command_window : string -> Coq.coqtop -> +class command_window : string -> Coq.coqtop -> CoqOps.coqops -> object method new_query : ?command:string -> ?term:string -> unit -> unit method pack_in : (GObj.widget -> unit) -> unit -- cgit v1.2.3