From: Claudio Sacerdoti Coen Date: Mon, 29 Apr 2002 10:23:17 +0000 (+0000) Subject: * Error handling improved X-Git-Tag: V_0_3_0_debian_8~118 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e562a5af68a5acfeacbf84fbe06ddf9f748f09df;p=helm.git * Error handling improved * Check does not move any more the input to the "old input" area. --- 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 ^ "

") ;