From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- ide/wg_Command.ml | 166 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 166 insertions(+) create mode 100644 ide/wg_Command.ml (limited to 'ide/wg_Command.ml') diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml new file mode 100644 index 00000000..7dad92ed --- /dev/null +++ b/ide/wg_Command.ml @@ -0,0 +1,166 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + 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 + +object(self) + val frame = frame + + val notebook = notebook + + 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 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 () -> + 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 = GText.view ~packing:r_bin#add () in + views <- (frame#coerce, result, combo#entry) :: views; + result#misc#modify_font current.text_font; + let clr = Tags.color_of_string current.background_color in + result#misc#modify_base [`NORMAL, `COLOR clr]; + 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 + 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 log level message = result#buffer#insert (message^"\n") in + let process = + Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function + | Interface.Fail (_,l,str) -> + result#buffer#insert str; + notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; + Coq.return () + | Interface.Good res -> + 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 + 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 + let _, _, e = + List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views in + e#misc#grab_focus () + + method hide = + frame#hide + + method visible = + frame#visible + + method refresh_font () = + let iter (_,view,_) = view#misc#modify_font current.text_font in + List.iter iter views + + method refresh_color () = + let clr = Tags.color_of_string current.background_color 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 (); + ignore(notebook#event#connect#key_press ~callback:(fun ev -> + if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true) + else false + )); + +end -- cgit v1.2.3