Reload stylesheets menu entry added (under the Settings menu)

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 83947a24abad3abde38ee1097d63f14c2020dc5c..5e6b181629204859824440fcdd40a261bf645575 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2764,12 +2764,21 @@ 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 () ;
+       refresh_proof output ;
+       refresh_goals notebook
+     ) in
  (* accel group *)
  let _ = window#add_accel_group accel_group in
  (* end of menus *)