Reload stylesheets menu entry added (under the Settings menu)

diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml
index 3a81e8b86062bc5f1b258cf8ba9fe7faf3ed616d..82060587acb91b31c06f8e0dee56fccde9cacd50 100644 (file)
--- a/helm/gTopLevel/applyStylesheets.ml
+++ b/helm/gTopLevel/applyStylesheets.ml
@@ -44,14 +44,31 @@ let parseStyle name =
   Gdome_xslt.processStylesheet style
 ;;
 
-let d_c = parseStyle "drop_coercions.xsl";;
-let tc1 = parseStyle "objtheorycontent.xsl";;
-let hc2 = parseStyle "content_to_html.xsl";;
-let l   = parseStyle "link.xsl";;
+let parseStyles () =
+ parseStyle "drop_coercions.xsl",
+ parseStyle "objtheorycontent.xsl",
+ parseStyle "content_to_html.xsl",
+ parseStyle "link.xsl",
+ parseStyle "rootcontent.xsl",
+ parseStyle "genmmlid.xsl",
+ parseStyle "annotatedpres.xsl"
+;;
+
+let (d_c,tc1,hc2,l,c1,g,c2) =
+ let (d_c,tc1,hc2,l,c1,g,c2) = parseStyles () in
+  ref d_c, ref tc1, ref hc2, ref l, ref c1, ref g, ref c2
+;;
 
-let c1 = parseStyle "rootcontent.xsl";;
-let g  = parseStyle "genmmlid.xsl";;
-let c2 = parseStyle "annotatedpres.xsl";;
+let reload_stylesheets () =
+ let (d_c',tc1',hc2',l',c1',g',c2') = parseStyles () in
+  d_c := d_c';
+  tc1 := tc1';
+  hc2 := hc2';
+  l   := l'  ;
+  c1  := c1' ;
+  g   := g'  ;
+  c2  := c2'
+;;
 
 
 let getterURL = Configuration.getter_url;;
@@ -100,7 +117,7 @@ let sequent_args =
 (** Stylesheets application **)
 
 let apply_stylesheets input styles args =
- List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
+ List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i !style args)
   input styles
 ;;
 

diff --git a/helm/gTopLevel/applyStylesheets.mli b/helm/gTopLevel/applyStylesheets.mli
index b450cd992db45bd41f678e3655ef4f53caa06404..c445d370834768d37ec875476deb7a0a65e1fb9a 100644 (file)
--- a/helm/gTopLevel/applyStylesheets.mli
+++ b/helm/gTopLevel/applyStylesheets.mli
@@ -33,6 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
+val reload_stylesheets : unit -> unit
+
 val mml_of_cic_sequent :
  Cic.metasenv ->
  int * Cic.context * Cic.term ->

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 *)