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/wg_Command.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'ide/wg_Command.ml') diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 47dad8f19..3fcb7ce49 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 -- cgit v1.2.3