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 04acbe2fac73c83a3408250387f9248322a1e7a2..eb50104af4f5a554e6c63aae5885d5e58c7ecb70 100644 (file)
--- 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;;