1 files changed, 181 insertions, 0 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
new file mode 100644
index 0000000000..06281d6287
--- /dev/null
+++ b/ide/wg_Command.ml
@@ -0,0 +1,181 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Preferences
+
+class command_window name coqtop coqops router =
+  let frame = Wg_Detachable.detachable
+    ~title:(Printf.sprintf "Query pane (%s)" name) () in
+  let _ = frame#hide in
+  let _ = GtkData.AccelGroup.create () in
+  let notebook =
+    GPack.notebook ~height:200 ~scrollable:true ~packing:frame#add () in
+  let _ = frame#connect#attached ~callback:(fun _ ->
+    notebook#misc#set_size_request ~height:200 ()) in
+  let _ = frame#connect#detached ~callback:(fun _ ->
+    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
+
+  val mutable views = []
+
+  method private new_page_maker =
+    let page = notebook#append_page
+      (GMisc.label ~text:"No query" ())#coerce in
+    let page = notebook#get_nth_page page in
+    let b = GButton.button () in
+    b#add (Ideutils.stock_to_widget ~size:(`CUSTOM(12,12)) `NEW);
+    ignore(b#connect#clicked ~callback:self#new_query);
+    notebook#set_page ~tab_label:b#coerce page;
+    new_page <- page
+
+  method new_query ?command ?term () = self#new_query_aux ?command ?term ()
+
+  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)));
+      b#add (Ideutils.stock_to_widget ~size:(`CUSTOM(12,10)) `CLOSE);
+      hbox#coerce in
+    notebook#set_page ~tab_label:(new_tab_lbl "New query") frame#coerce;
+    notebook#goto_page (notebook#page_num frame#coerce);
+    let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
+    let combo, entry, ok_b =
+      let bar =
+        GButton.toolbar ~style:`ICONS ~packing:(vbox#pack ~expand:false) () in
+      let bar_add ~expand w =
+        let item = GButton.tool_item ~expand () in
+        item#add w#coerce;
+        bar#insert item in
+      let combo, _ =
+        GEdit.combo_box_entry_text ~strings:Coq_commands.state_preserving () in
+      combo#entry#set_text "Search";
+      let entry = GEdit.entry () in
+      entry#misc#set_can_default true;
+      let ok_b = GButton.button () in
+      ok_b#add (Ideutils.stock_to_widget `OK);
+      bar_add ~expand:false combo;
+      bar_add ~expand:true entry;
+      bar_add ~expand:false ok_b;
+      combo, entry, ok_b in
+    let r_bin =
+      GBin.scrolled_window
+	~vpolicy:`AUTOMATIC
+	~hpolicy:`AUTOMATIC
+	~packing:(vbox#pack ~fill:true ~expand:true) () in
+    let result = Wg_MessageView.message_view () in
+    router#register_route route_id result;
+    r_bin#add_with_viewport (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 ~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 *)
+    let callback () =
+      let com = combo#entry#text in
+      let arg = entry#text in
+      if Str.string_match (Str.regexp "^ *$") (com^arg) 0 then () else
+      let phrase =
+        if Str.string_match (Str.regexp "\\. *$") com 0 then com
+        else com ^ " " ^ arg ^" . "
+      in
+      let process =
+        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 () ->
+            notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
+            Coq.return ()
+        in
+        coqops#raw_coq_query ~route_id ~next phrase
+      in
+      result#set (Pp.str ("Result for command " ^ phrase ^ ":\n"));
+      Coq.try_grab coqtop process ignore
+    in
+    ignore (combo#entry#connect#activate ~callback);
+    ignore (ok_b#connect#clicked ~callback);
+    begin match command with
+      | None -> ()
+      | Some c -> combo#entry#set_text c
+    end;
+    begin match term with
+      | None -> ()
+      | Some t -> entry#set_text t
+    end;
+    combo#entry#misc#grab_focus ();
+    if grab_now then entry#misc#grab_default ();
+    ignore (entry#connect#activate ~callback);
+    ignore (combo#entry#connect#activate ~callback);
+    ignore (combo#entry#event#connect#key_press ~callback:(fun ev ->
+      if GdkEvent.Key.keyval ev = GdkKeysyms._Tab then
+        (entry#misc#grab_focus ();true)
+      else false))
+
+  method show =
+    frame#show;
+    let cur_page = notebook#get_nth_page notebook#current_page in
+    match List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views with
+    | (_, _, e) -> e#misc#grab_focus ()
+    | exception Not_found -> ()
+
+  method hide =
+    frame#hide
+
+  method visible =
+    frame#visible
+
+  method private refresh_color clr =
+    let clr = Tags.color_of_string clr in
+    let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in
+    List.iter iter views
+
+  initializer
+    self#new_page_maker;
+    self#new_query_aux ~grab_now:false ();
+    frame#misc#hide ();
+    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)
+      else false
+    ));
+
+end