(* 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 =
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
;;
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 () =
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
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
projects / helm.git / blobdiff