diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-19 23:24:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-20 00:15:12 +0200 |
| commit | 61b946cde62d3324c39f663974d4cfadd9207a69 (patch) | |
| tree | 3c87d311bc63ae3aadd878a51cf5813f820ef495 /ide/wg_Command.ml | |
| parent | b3ed40b82540639de925afd36a32fbd716d2800f (diff) | |
[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.
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 13 |
1 files changed, 11 insertions, 2 deletions
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 |