* 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 f6556ed8c58614589af187b497486ffc8e6c4cb4..905de741041dc586772fbac7fa5f6c5224a53031 100644 (file)
--- 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
          ("<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 ;
@@ -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
-           ("<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>")
+         | RefreshProofException e ->
+            output_html outputhtml
+             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+              "proof: " ^ Printexc.to_string e ^ "</h1>")
+         | e ->
+            output_html outputhtml
+             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
        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
-      ("<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>")
+    | RefreshProofException e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+         "proof: " ^ Printexc.to_string e ^ "</h1>")
+    | e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
 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
+         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+          "sequent: " ^ Printexc.to_string e ^ "</h1>")
+     | RefreshProofException e ->
+        output_html outputhtml
+         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+          "proof: " ^ Printexc.to_string e ^ "</h1>")
      | e ->
         output_html outputhtml
          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
@@ -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
         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;