X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=f6556ed8c58614589af187b497486ffc8e6c4cb4;hb=9b5c1945c6d3af81f07c41da187404c2431cefa3;hp=268d2846ee853b1613a7fa2e08d6d0ab584f5279;hpb=faf01084c13ccd731d7040fadb96caa0a2aa0019;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 268d2846e..f6556ed8c 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -165,50 +165,60 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 
 (* CALLBACKS *)
 
+exception RefreshSequentException of exn;;
+exception RefreshProofException of exn;;
+
 let refresh_proof (output : GMathView.math_view) =
- let uri,currentproof =
-  match !ProofEngine.proof with
-     None -> assert false
-   | Some (uri,metasenv,bo,ty) ->
-      uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
- in
- let
-  (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
- =
-  Cic2acic.acic_object_of_cic_object currentproof
- in
-  let mml = mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types in
-   output#load_tree mml ;
-   current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+ try
+  let uri,currentproof =
+   match !ProofEngine.proof with
+      None -> assert false
+    | Some (uri,metasenv,bo,ty) ->
+       uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
+  in
+   let
+    (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
+   =
+    Cic2acic.acic_object_of_cic_object currentproof
+   in
+    let mml =
+     mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
+    in
+     output#load_tree mml ;
+     current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+ with
+  e -> raise (RefreshProofException e)
 ;;
 
 let refresh_sequent (proofw : GMathView.math_view) =
- match !ProofEngine.goal with
-    None -> proofw#unload
-  | Some (_,currentsequent) ->
-     let metasenv =
-      match !ProofEngine.proof with
-         None -> assert false
-       | Some (_,metasenv,_,_) -> metasenv
-     in
-      let sequent_gdome,ids_to_terms,ids_to_father_ids =
-       SequentPp.XmlPp.print_sequent metasenv currentsequent
+ try
+  match !ProofEngine.goal with
+     None -> proofw#unload
+   | Some (_,currentsequent) ->
+      let metasenv =
+       match !ProofEngine.proof with
+          None -> assert false
+        | Some (_,metasenv,_,_) -> metasenv
       in
-       let sequent_doc =
-        Xml2Gdome.document_of_xml domImpl sequent_gdome
+       let sequent_gdome,ids_to_terms,ids_to_father_ids =
+        SequentPp.XmlPp.print_sequent metasenv currentsequent
        in
-        let sequent_mml =
-         applyStylesheets sequent_doc sequent_styles sequent_args
+        let sequent_doc =
+         Xml2Gdome.document_of_xml domImpl sequent_gdome
         in
-         proofw#load_tree ~dom:sequent_mml ;
-         current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
+         let sequent_mml =
+          applyStylesheets sequent_doc sequent_styles sequent_args
+         in
+          proofw#load_tree ~dom:sequent_mml ;
+          current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
+ with
+  e -> raise (RefreshSequentException e)
+;;
+
 (*
 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
  ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
-ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
- ~name:"/public/sacerdot/guruguru2" ~indent:true ())
 *)
-;;
 
 let mml_of_cic_term term =
  let context =
@@ -256,11 +266,26 @@ let call_tactic tactic rendering_window () =
     refresh_sequent proofw ;
     refresh_proof output
    with
-    e ->
-     output_html outputhtml
-      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-     ProofEngine.proof := savedproof ;
-     ProofEngine.goal := savedgoal ;
+      RefreshSequentException e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+         "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal ;
+       refresh_sequent proofw
+    | RefreshProofException e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+         "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal ;
+       refresh_sequent proofw ;
+       refresh_proof output
+    | e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal ;
   end
 ;;
 
@@ -304,11 +329,33 @@ let call_tactic_with_input tactic rendering_window () =
     with
        CicTextualParser0.Eof ->
         inputt#delete_text 0 inputlen
+     | RefreshSequentException e ->
+        output_html outputhtml
+         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+        ProofEngine.proof := savedproof ;
+        ProofEngine.goal := savedgoal ;
+        refresh_sequent proofw
+     | RefreshProofException e ->
+        output_html outputhtml
+         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+prerr_endline "PROVA CHE FA SOLLEVARE UN'ECCEZIONE:" ; flush stderr ;
+begin
+match !ProofEngine.proof with Some (_,metasenv,bo,_) ->
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^
+CicPp.ppterm ty) ; flush stderr) metasenv ;
+prerr_endline ("PROOF: " ^ CicPp.ppterm bo) ; flush stderr ;
+end ;
+        ProofEngine.proof := savedproof ;
+        ProofEngine.goal := savedgoal ;
+        refresh_sequent proofw ;
+        refresh_proof output
      | e ->
         output_html outputhtml
-         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>");
+         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
         ProofEngine.proof := savedproof ;
-        ProofEngine.goal := savedgoal
+        ProofEngine.goal := savedgoal ;
 ;;
 
 let call_tactic_with_goal_input tactic rendering_window () =
@@ -338,9 +385,26 @@ let call_tactic_with_goal_input tactic rendering_window () =
                refresh_proof rendering_window#output
            | None -> assert false (* "ERROR: No current term!!!" *)
          with
-          e ->
-           output_html outputhtml
-            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+            RefreshSequentException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw
+          | RefreshProofException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw ;
+             refresh_proof output
+          | e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
         end
    | None ->
       output_html outputhtml
@@ -409,9 +473,26 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
                  end
            | None -> assert false (* "ERROR: No current term!!!" *)
          with
-          e ->
-           output_html outputhtml
-            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+            RefreshSequentException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw
+          | RefreshProofException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw ;
+             refresh_proof output
+          | e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
         end
    | None ->
       output_html outputhtml