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
~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
~callback:
(function _ ->
ApplyStylesheets.reload_stylesheets () ;
- refresh_proof output ;
- refresh_goals notebook
+ 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