(* 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";;
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
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
~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
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 *)