Reloading bugged stylesheets no longer makes gTopLevel crash.

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e3f49893171f5c9e1faaa01931ff9a76eef72a77..d71162d1e5b3b058e89519444f8a930e7938a299 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -43,7 +43,10 @@ module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
 
+let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
+(*
 let mqi_flags = [] (* default MathQL interpreter options *)
+*)
 let mqi_handle = MQIC.init mqi_flags prerr_string
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
@@ -1920,7 +1923,16 @@ let completeSearchPattern () =
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
    let must = MQueryLevels2.get_constraints expr in
    let must',only = refine_constraints must in
-   let query = MQG.query_of_constraints None must' only in
+   let query =
+    MQG.query_of_constraints
+     (Some
+       ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
+        "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
+        "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
+        "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"
+       ])
+     must' only
+   in
    let results = MQI.execute mqi_handle query in 
     show_query_results results
   with
@@ -2752,12 +2764,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 *)