From: Claudio Sacerdoti Coen Date: Mon, 18 Nov 2002 18:41:56 +0000 (+0000) Subject: Interface improvement (???): the Check button has been moved to a brand new X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a9e833b37216b225262450fd4e3fa5bf79ae4c3a;p=helm.git Interface improvement (???): the Check button has been moved to a brand new menu. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 04acbe2fa..eb50104af 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -152,10 +152,10 @@ Arg.parse argspec ignore "" (* A WIDGET TO ENTER CIC TERMS *) -class term_editor ?packing ?width ?height ?changed_callback () = +class term_editor ?packing ?width ?height ?isnotempty_callback () = let input = GEdit.text ~editable:true ?width ?height ?packing () in let _ = - match changed_callback with + match isnotempty_callback with None -> () | Some callback -> ignore(input#connect#changed (function () -> callback (input#length > 0))) @@ -1368,7 +1368,7 @@ let new_proof () = (* moved here to have visibility of the ok button *) let newinputt = new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add () - ~changed_callback: + ~isnotempty_callback: (function b -> non_empty_type := b ; okb#misc#set_sensitive (b && uri_entry#text <> "")) @@ -1730,7 +1730,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () = let module L = LogicalOperations in let module G = Gdome in let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in - let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in match mmlwidget#get_selection with @@ -2156,7 +2156,7 @@ end;; (* Scratch window *) -class scratch_window outputhtml = +class scratch_window = let window = GWindow.window ~title:"MathML viewer" ~border_width:2 () in let vbox = @@ -2179,7 +2179,6 @@ class scratch_window outputhtml = GMathView.math_view ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) - method outputhtml = outputhtml method mmlwidget = mmlwidget method show () = window#misc#hide () ; window#show () initializer @@ -2395,6 +2394,7 @@ end (* Main window *) class rendering_window output (notebook : notebook) = + let scratch_window = new scratch_window in let window = GWindow.window ~title:"MathML viewer" ~border_width:0 ~allow_shrink:false () in @@ -2419,7 +2419,7 @@ class rendering_window output (notebook : notebook) = ~callback:open_ in let qed_menu_item = - factory1#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in + factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in ignore (factory1#add_separator ()) ; ignore (factory1#add_item "Load Unfinished Proof" ~key:GdkKeysyms._L @@ -2434,15 +2434,15 @@ class rendering_window output (notebook : notebook) = ignore (!qed_set_sensitive false); ignore (factory1#add_separator ()) ; let export_to_postscript_menu_item = - factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E + factory1#add_item "Export to PostScript..." ~callback:(export_to_postscript output) in ignore (factory1#add_separator ()) ; ignore - (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ; + (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ; export_to_postscript_menu_item end in (* edit menu *) - let edit_menu = factory0#add_submenu "Edit current proof" in + let edit_menu = factory0#add_submenu "Edit Current Proof" in let factory2 = new GMenu.factory edit_menu ~accel_group in let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in let proveit_menu_item = @@ -2460,6 +2460,13 @@ class rendering_window output (notebook : notebook) = focus_menu_item#misc#set_sensitive b in let _ = !focus_and_proveit_set_sensitive false in + (* edit term menu *) + let edit_term_menu = factory0#add_submenu "Edit Term" in + let factory5 = new GMenu.factory edit_term_menu ~accel_group in + let check_menu_item = + factory5#add_item "Check Term" ~key:GdkKeysyms._C + ~callback:(check scratch_window) in + let _ = check_menu_item#misc#set_sensitive false in (* search menu *) let settings_menu = factory0#add_submenu "Search" in let factory4 = new GMenu.factory settings_menu ~accel_group in @@ -2492,20 +2499,14 @@ class rendering_window output (notebook : notebook) = ~packing:(vbox#pack ~expand:true ~padding:5) () in let _ = scrolled_window0#add output#coerce in let frame = - GBin.frame ~label:"Term input" + GBin.frame ~label:"Insert Term" ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let vbox' = - GPack.vbox ~packing:frame#add () in - let hbox4 = - GPack.hbox ~border_width:5 ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let scrolled_window1 = GBin.scrolled_window ~border_width:5 - ~packing:(vbox'#pack ~expand:true ~padding:0) () in + ~packing:frame#add () in let inputt = - new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () in + new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () + ~isnotempty_callback:check_menu_item#misc#set_sensitive in let vboxl = GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let _ = @@ -2520,7 +2521,6 @@ class rendering_window output (notebook : notebook) = ~border_width:20 ~packing:frame#add ~show:true () in - let scratch_window = new scratch_window outputhtml in object method outputhtml = outputhtml method inputt = inputt @@ -2544,7 +2544,6 @@ object set_settings_window settings_window ; set_outputhtml outputhtml ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; - ignore(checkb#connect#clicked (check scratch_window)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) end;;