diff options
| -rw-r--r-- | ide/session.ml | 2 | ||||
| -rw-r--r-- | ide/wg_Command.ml | 13 | ||||
| -rw-r--r-- | 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 |