diff options
| -rw-r--r-- | ide/command_windows.ml | 24 | ||||
| -rw-r--r-- | ide/command_windows.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 28 |
3 files changed, 37 insertions, 17 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 939238d3a3..a34e5ebeb3 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -13,6 +13,7 @@ class command_window coqtop current = ~position:`CENTER ~title:"CoqIde queries" ~show:false () in *) + let views = ref [] in let frame = GBin.frame ~label:"Command Pane" ~shadow_type:`IN () in let _ = frame#misc#hide () in let _ = GtkData.AccelGroup.create () in @@ -49,12 +50,17 @@ class command_window coqtop current = () in + let remove_cb () = + let index = notebook#current_page in + let () = notebook#remove_page index in + views := Minilib.list_filter_i (fun i x -> i <> index) !views + in let _ = toolbar#insert_button ~tooltip:"Delete Page" ~text:"Delete Page" ~icon:(Ideutils.stock_to_widget `DELETE) - ~callback:(fun () -> notebook#remove_page notebook#current_page) + ~callback:remove_cb () in object(self) @@ -63,14 +69,14 @@ object(self) val new_page_menu = new_page_menu val notebook = notebook + method frame = frame method new_command ?command ?term () = - let appendp x = ignore (notebook#append_page x) in let frame = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:appendp () in + let _ = notebook#append_page frame#coerce in notebook#goto_page (notebook#page_num frame#coerce); let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in @@ -91,7 +97,10 @@ object(self) ~packing:(vbox#pack ~fill:true ~expand:true) () in let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in let result = GText.view ~packing:r_bin#add () in + let () = views := !views @ [result] in result#misc#modify_font !current.Preferences.text_font; + let clr = Tags.color_of_string !current.Preferences.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 () = @@ -134,6 +143,15 @@ object(self) ignore (combo#entry#connect#activate ~callback); self#frame#misc#show () + method refresh_font () = + let iter view = view#misc#modify_font !current.Preferences.text_font in + List.iter iter !views + + method refresh_color () = + let clr = Tags.color_of_string !current.Preferences.background_color in + let iter view = view#misc#modify_base [`NORMAL, `COLOR clr] in + List.iter iter !views + initializer ignore (new_page_menu#connect#clicked ~callback:self#new_command); (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*) diff --git a/ide/command_windows.mli b/ide/command_windows.mli index 8c7319aa3d..c34b6cf67a 100644 --- a/ide/command_windows.mli +++ b/ide/command_windows.mli @@ -11,4 +11,6 @@ class command_window : object method new_command : ?command:string -> ?term:string -> unit -> unit method frame : GBin.frame + method refresh_font : unit -> unit + method refresh_color : unit -> unit end diff --git a/ide/coqide.ml b/ide/coqide.ml index 358302d3c4..a299ffda00 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2804,24 +2804,24 @@ let main files = refresh_font_hook := (fun () -> let fd = !current.text_font in - List.iter - (fun {script=view; proof_view=prf_v; message_view=msg_v} -> - view#misc#modify_font fd; - prf_v#misc#modify_font fd; - msg_v#misc#modify_font fd - ) - session_notebook#pages; + let iter_page p = + p.script#misc#modify_font fd; + p.proof_view#misc#modify_font fd; + p.message_view#misc#modify_font fd; + p.command#refresh_font () + in + List.iter iter_page session_notebook#pages; ); refresh_background_color_hook := (fun () -> let clr = Tags.color_of_string !current.background_color in - List.iter - (fun {script=view; proof_view=prf_v; message_view=msg_v} -> - view#misc#modify_base [`NORMAL, `COLOR clr]; - prf_v#misc#modify_base [`NORMAL, `COLOR clr]; - msg_v#misc#modify_base [`NORMAL, `COLOR clr] - ) - session_notebook#pages; + let iter_page p = + p.script#misc#modify_base [`NORMAL, `COLOR clr]; + p.proof_view#misc#modify_base [`NORMAL, `COLOR clr]; + p.message_view#misc#modify_base [`NORMAL, `COLOR clr]; + p.command#refresh_color () + in + List.iter iter_page session_notebook#pages; ); resize_window_hook := (fun () -> w#resize |