* Error reporting improved

* Check now also works when no current goal and/or no current proof is
  available.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index eb02cb07f8e88b9a69204ab8cdfd637a88b9472d..800e69aa07b485cd326638ad3b3f5ba33caee01c 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -300,7 +300,6 @@ let call_tactic_with_input tactic rendering_window () =
        CicTextualParser0.Eof ->
         inputt#delete_text 0 inputlen
      | e ->
-prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
         output_html outputhtml
          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>");
         ProofEngine.proof := savedproof ;
@@ -335,7 +334,6 @@ let call_tactic_with_goal_input tactic rendering_window () =
            | None -> assert false (* "ERROR: No current term!!!" *)
          with
           e ->
-           prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
            output_html outputhtml
             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
         end
@@ -405,7 +403,6 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
            | None -> assert false (* "ERROR: No current term!!!" *)
          with
           e ->
-prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
            output_html outputhtml
             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
         end
@@ -481,31 +478,34 @@ let save rendering_window () =
 let proveit rendering_window () =
  let module L = LogicalOperations in
  let module G = Gdome in
- match rendering_window#output#get_selection with
-   Some node ->
-    let xpath =
-     ((node : Gdome.element)#getAttributeNS
-     (*CSC: OCAML DIVERGE
-     ((element : G.element)#getAttributeNS
-     *)
-       ~namespaceURI:helmns
-       ~localName:(G.domString "xref"))#to_string
-    in
-     if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-     else
-      begin
-       try
-        match !current_cic_infos with
-           Some (ids_to_terms, ids_to_father_ids) ->
-            let id = xpath in
-             if L.to_sequent id ids_to_terms ids_to_father_ids then
-              refresh_proof rendering_window#output ;
-             refresh_sequent rendering_window#proofw
-         | None -> assert false (* "ERROR: No current term!!!" *)
-       with
-        e -> print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
-      end
- | None -> assert false (* "ERROR: No selection!!!" *)
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+  match rendering_window#output#get_selection with
+    Some node ->
+     let xpath =
+      ((node : Gdome.element)#getAttributeNS
+      (*CSC: OCAML DIVERGE
+      ((element : G.element)#getAttributeNS
+      *)
+        ~namespaceURI:helmns
+        ~localName:(G.domString "xref"))#to_string
+     in
+      if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+      else
+       begin
+        try
+         match !current_cic_infos with
+            Some (ids_to_terms, ids_to_father_ids) ->
+             let id = xpath in
+              if L.to_sequent id ids_to_terms ids_to_father_ids then
+               refresh_proof rendering_window#output ;
+              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>")
+       end
+  | None -> assert false (* "ERROR: No selection!!!" *)
 ;;
 
 exception NotADefinition;;
@@ -576,12 +576,12 @@ let state rendering_window () =
         inputt#delete_text 0 inputlen ;
         ignore(oldinputt#insert_text input oldinputt#length)
      | e ->
-        print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+        output_html outputhtml
+         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
 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
@@ -589,13 +589,13 @@ let check rendering_window scratch_window () =
   let input = inputt#get_chars 0 inputlen ^ "\n" in
   let curi,metasenv =
    match !ProofEngine.proof with
-      None -> assert false
+      None -> UriManager.uri_of_string "cic:/dummy.con", []
     | Some (curi,metasenv,_,_) -> curi,metasenv
   in
   let ciccontext,names_context =
    let context =
     match !ProofEngine.goal with
-       None -> assert false
+       None -> []
      | Some (_,(ctx,_)) -> ctx
    in
     ProofEngine.cic_context_of_context context,
@@ -624,10 +624,10 @@ let check rendering_window scratch_window () =
      done
     with
        CicTextualParser0.Eof ->
-        inputt#delete_text 0 inputlen ;
-        ignore(oldinputt#insert_text input oldinputt#length)
+        inputt#delete_text 0 inputlen
      | e ->
-        print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+       output_html outputhtml
+        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
 let choose_selection
@@ -786,7 +786,7 @@ object(self)
  method display = mmlwidget#load_tree
  method show = window#show
  initializer
-  ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
+  ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
 end;;
 
 (* Main window *)