From 9db3b8bbda8724f2b0fca7e84cecb68a5490c369 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 27 Jun 2003 13:07:34 +0000 Subject: [PATCH] Reload stylesheets menu entry added (under the Settings menu) --- helm/gTopLevel/applyStylesheets.ml | 33 ++++++++++++++++++++++------- helm/gTopLevel/applyStylesheets.mli | 2 ++ helm/gTopLevel/gTopLevel.ml | 11 +++++++++- 3 files changed, 37 insertions(+), 9 deletions(-) diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml index 3a81e8b86..82060587a 100644 --- 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 b450cd992..c445d3708 100644 --- 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 83947a24a..5e6b18162 100644 --- 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 *) -- 2.39.2