- default font size of the proof window lowered to 10

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 83947a24abad3abde38ee1097d63f14c2020dc5c..0ceb6f2af7a8d436a0831cc8a6c9725893ecf66b 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1653,7 +1653,8 @@ let open_ () =
        Some (uri, metasenv, bo, ty) ;
       ProofEngine.goal := None ;
       refresh_goals notebook ;
-      refresh_proof output
+      refresh_proof output ;
+      !save_set_sensitive true
    with
       InvokeTactics.RefreshSequentException e ->
        output_html outputhtml
@@ -2273,7 +2274,8 @@ class settings_window output sw
    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
  let font_size_spinb =
   let sadj =
-   GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
+   GData.adjustment ~value:(float_of_int output#get_font_size)
+    ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
   in
    GEdit.spin_button 
     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
@@ -2764,12 +2766,34 @@ class rendering_window output (notebook : notebook) =
  let settings_menu = factory0#add_submenu "Settings" in
  let factory3 = new GMenu.factory settings_menu ~accel_group in
  let _ =
-  factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
+  factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A
    ~callback:edit_aliases in
  let _ = factory3#add_separator () in
  let _ =
   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
    ~callback:(function _ -> (settings_window ())#show ()) in
+ let _ = factory3#add_separator () in
+ let _ =
+  factory3#add_item "Reload Stylesheets"
+   ~callback:
+     (function _ ->
+       ApplyStylesheets.reload_stylesheets () ;
+       if !ProofEngine.proof <> None then
+        try
+         refresh_goals notebook ;
+         refresh_proof output
+        with
+           InvokeTactics.RefreshSequentException e ->
+            output_html (outputhtml ())
+             ("<h1 color=\"red\">An error occurred while refreshing the " ^
+               "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+           (*notebook#remove_all_pages ~skip_switch_page_event:false ;*)
+           notebook#set_empty_page
+         | InvokeTactics.RefreshProofException e ->
+            output_html (outputhtml ())
+             ("<h1 color=\"red\">An error occurred while refreshing the proof: "               ^ Printexc.to_string e ^ "</h1>") ;
+            output#unload
+     ) in
  (* accel group *)
  let _ = window#add_accel_group accel_group in
  (* end of menus *)