diff options
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 56 |
1 files changed, 34 insertions, 22 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 946aaf01..8eddfb31 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Preferences -class command_window name coqtop = +class command_window name coqtop coqops router = let frame = Wg_Detachable.detachable ~title:(Printf.sprintf "Query pane (%s)" name) () in let _ = frame#hide in @@ -21,11 +23,20 @@ class command_window name coqtop = notebook#misc#set_size_request ~width:600 ~height:500 (); notebook#misc#grab_focus ()) in + let route_id = + let r = ref 0 in + fun () -> incr r; !r in + object(self) val frame = frame 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 @@ -47,11 +58,13 @@ object(self) method private new_query_aux ?command ?term ?(grab_now=true) () = let frame = GBin.frame ~shadow_type:`NONE () in ignore(notebook#insert_page ~pos:(notebook#page_num new_page) frame#coerce); + let route_id = route_id () in let new_tab_lbl text = let hbox = GPack.hbox ~homogeneous:false () in ignore(GMisc.label ~width:100 ~ellipsize:`END ~text ~packing:hbox#pack()); let b = GButton.button ~packing:hbox#pack () in ignore(b#connect#clicked ~callback:(fun () -> + router#delete_route route_id; views <- List.filter (fun (f,_,_) -> f#get_oid <> frame#coerce#get_oid) views; notebook#remove_page (notebook#page_num frame#coerce))); @@ -83,15 +96,16 @@ object(self) ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(vbox#pack ~fill:true ~expand:true) () in - let result = GText.view ~packing:r_bin#add () in + let result = Wg_MessageView.message_view () in + router#register_route route_id result; + r_bin#add (result :> GObj.widget); views <- (frame#coerce, result, combo#entry) :: views; let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = result#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in stick text_font result cb; result#misc#set_can_focus true; (* false causes problems for selection *) - result#set_editable false; let callback () = let com = combo#entry#text in let arg = entry#text in @@ -100,22 +114,20 @@ object(self) if Str.string_match (Str.regexp "\\. *$") com 0 then com else com ^ " " ^ arg ^" . " in - let log level message = - Ideutils.insert_xml result#buffer message; - result#buffer#insert "\n"; - in let process = - Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function - | Interface.Fail (_,l,str) -> - Ideutils.insert_xml result#buffer str; + let next = function + | Interface.Fail (_, _, err) -> + let err = Ideutils.validate err in + result#set err; notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; - Coq.return () - | Interface.Good res -> - result#buffer#insert res; + Coq.return () + | Interface.Good () -> notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce; - Coq.return ()) + Coq.return () + in + coqops#raw_coq_query ~route_id ~next phrase in - result#buffer#set_text ("Result for command " ^ phrase ^ ":\n"); + result#set (Pp.str ("Result for command " ^ phrase ^ ":\n")); Coq.try_grab coqtop process ignore in ignore (combo#entry#connect#activate ~callback); @@ -159,7 +171,7 @@ object(self) self#new_page_maker; self#new_query_aux ~grab_now:false (); frame#misc#hide (); - let _ = background_color#connect#changed self#refresh_color in + let _ = background_color#connect#changed ~callback:self#refresh_color in self#refresh_color background_color#get; ignore(notebook#event#connect#key_press ~callback:(fun ev -> if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true) |