X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=905de741041dc586772fbac7fa5f6c5224a53031;hb=e562a5af68a5acfeacbf84fbe06ddf9f748f09df;hp=f6556ed8c58614589af187b497486ffc8e6c4cb4;hpb=2a40efede6d4430b4ca086275bcac80905ec1a74;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f6556ed8c..905de7410 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -83,12 +83,6 @@ let c2 = parseStyle "annotatedpres.xsl";;
let getterURL = Configuration.getter_url;;
let processorURL = Configuration.processor_url;;
-(*
-let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";;
-let getterURL = "http://phd.cs.unibo.it:8081/";;
-let processorURL = "http://localhost:8080/helm/servelt/uwobo/";;
-let getterURL = "http://localhost:8081/";;
-*)
let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
let mml_args =
@@ -340,13 +334,6 @@ let call_tactic_with_input tactic rendering_window () =
output_html outputhtml
("
Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "
") ;
-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 ;
@@ -642,9 +629,17 @@ let proveit rendering_window () =
refresh_sequent rendering_window#proofw
| None -> assert false (* "ERROR: No current term!!!" *)
with
- e ->
- output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
")
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "
")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "
")
+ | e ->
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
")
end
| None -> assert false (* "ERROR: No selection!!!" *)
;;
@@ -673,14 +668,22 @@ let open_ rendering_window () =
ProofEngine.proof :=
Some (uri, metasenv, bo, ty) ;
ProofEngine.goal := None ;
- inputt#delete_text 0 inputlen ;
- ignore(oldinputt#insert_text input oldinputt#length) ;
refresh_sequent proofw ;
refresh_proof output ;
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length)
with
- e ->
- output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "
")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "
")
+ | e ->
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
") ;
;;
let state rendering_window () =
@@ -699,23 +702,26 @@ let state rendering_window () =
match CicTextualParser.main CicTextualLexer.token lexbuf with
None -> ()
| Some expr ->
- try
- let _ = CicTypeChecker.type_of_aux' [] [] expr in
- ProofEngine.proof :=
- Some (UriManager.uri_of_string "cic:/dummy.con",
- [1,expr], Cic.Meta 1, expr) ;
- ProofEngine.goal := Some (1,([],expr)) ;
- refresh_sequent proofw ;
- refresh_proof output ;
- with
- e ->
- print_endline ("? " ^ CicPp.ppterm expr) ;
- raise e
+ let _ = CicTypeChecker.type_of_aux' [] [] expr in
+ ProofEngine.proof :=
+ Some (UriManager.uri_of_string "cic:/dummy.con",
+ [1,expr], Cic.Meta 1, expr) ;
+ ProofEngine.goal := Some (1,([],expr)) ;
+ refresh_sequent proofw ;
+ refresh_proof output ;
done
with
CicTextualParser0.Eof ->
inputt#delete_text 0 inputlen ;
ignore(oldinputt#insert_text input oldinputt#length)
+ | RefreshSequentException e ->
+ output_html outputhtml
+ ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "
")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "
")
| e ->
output_html outputhtml
("" ^ Printexc.to_string e ^ "
") ;
@@ -723,7 +729,6 @@ let state rendering_window () =
let check rendering_window scratch_window () =
let inputt = (rendering_window#inputt : GEdit.text) in
- let oldinputt = (rendering_window#oldinputt : GEdit.text) in
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
let output = (rendering_window#output : GMathView.math_view) in
let proofw = (rendering_window#proofw : GMathView.math_view) in
@@ -769,9 +774,7 @@ let check rendering_window scratch_window () =
raise e
done
with
- CicTextualParser0.Eof ->
- inputt#delete_text 0 inputlen ;
- ignore(oldinputt#insert_text input oldinputt#length)
+ CicTextualParser0.Eof -> ()
| e ->
output_html outputhtml
("" ^ Printexc.to_string e ^ "
") ;