From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 27 Jun 2003 13:51:55 +0000 (+0000)
Subject: Reloading bugged stylesheets no longer makes gTopLevel crash.
X-Git-Tag: camera_ready~39
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eac698cf60e63383781fac2810981dface465216;p=helm.git

Reloading bugged stylesheets no longer makes gTopLevel crash.
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 5e6b18162..d71162d1e 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2776,8 +2776,21 @@ class rendering_window output (notebook : notebook) =
    ~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