From: Luca Padovani <luca.padovani@unito.it>
Date: Tue, 4 Nov 2003 10:49:02 +0000 (+0000)
Subject: * first upgrade to the new error logging mechanism
X-Git-Tag: V_0_2_2~33
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=909551e6f7511de1fcb84914baa4c909e33845ee;p=helm.git

* first upgrade to the new error logging mechanism
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9fd0b352b..6aaec3aed 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -180,9 +180,7 @@ let string_of_cic_textual_parser_uri uri =
 ;;
 
 let output_html outputhtml msg =
- htmlheader_and_content := !htmlheader_and_content ^ msg ;
- outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
- outputhtml#set_topline (-1)
+ outputhtml#log msg
 ;;
 
 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
@@ -221,7 +219,7 @@ let check_window outputhtml uris =
          with
           e ->
            output_html outputhtml
-            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+            (`Error (`T (Printexc.to_string e)))
        )
    ) uris
  in
@@ -511,12 +509,10 @@ let save_unfinished_proof () =
  let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
  Xml.pp ~quiet:true xml (Some prooffiletype) ;
  output_html outputhtml
-  ("<h1 color=\"Green\">Current proof type saved to " ^
-   prooffiletype ^ "</h1>") ;
+  (`Msg (`T ("Current proof type saved to " ^ prooffiletype))) ;
  Xml.pp ~quiet:true bodyxml (Some prooffile) ;
  output_html outputhtml
-  ("<h1 color=\"Green\">Current proof body saved to " ^
-   prooffile ^ "</h1>")
+  (`Msg (`T ("Current proof body saved to " ^ prooffile)))
 ;;
 
 (* Used to typecheck the loaded proofs *)
@@ -672,7 +668,7 @@ module InvokeTacticsCallbacks =
 
   let decompose_uris_choice_callback = decompose_uris_choice_callback
   let mk_fresh_name_callback = mk_fresh_name_callback
-  let output_html msg = output_html (outputhtml ()) msg
+  let output_html msg = output_html (outputhtml ()) (`Msg (`T msg))
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
@@ -716,25 +712,25 @@ let load_unfinished_proof () =
              ) ;
             refresh_goals notebook ;
              output_html outputhtml
-              ("<h1 color=\"Green\">Current proof type loaded from " ^
-                prooffiletype ^ "</h1>") ;
+              (`Msg (`T ("Current proof type loaded from " ^
+                prooffiletype))) ;
              output_html outputhtml
-              ("<h1 color=\"Green\">Current proof body loaded from " ^
-                prooffile ^ "</h1>") ;
+              (`Msg (`T ("Current proof body loaded from " ^
+                prooffile))) ;
             !save_set_sensitive true;
          | _ -> assert false
   with
      InvokeTactics.RefreshSequentException e ->
       output_html outputhtml
-       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-        "sequent: " ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e)))
    | InvokeTactics.RefreshProofException e ->
       output_html outputhtml
-       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-        "proof: " ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e)))
    | e ->
       output_html outputhtml
-       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+       (`Error (`T (Printexc.to_string e)))
 ;;
 
 let edit_aliases () =
@@ -838,15 +834,15 @@ let proveit () =
   with
      InvokeTactics.RefreshSequentException e ->
       output_html outputhtml
-       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-        "sequent: " ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e)))
    | InvokeTactics.RefreshProofException e ->
       output_html outputhtml
-       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-        "proof: " ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e)))
    | e ->
       output_html outputhtml
-       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T (Printexc.to_string e)))
 ;;
 
 let focus () =
@@ -861,15 +857,15 @@ let focus () =
   with
      InvokeTactics.RefreshSequentException e ->
       output_html outputhtml
-       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-        "sequent: " ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e)))
    | InvokeTactics.RefreshProofException e ->
       output_html outputhtml
-       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-        "proof: " ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e)))
    | e ->
       output_html outputhtml
-       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T (Printexc.to_string e)))
 ;;
 
 exception NoPrevGoal;;
@@ -879,7 +875,8 @@ let setgoal metano =
  let module L = LogicalOperations in
  let module G = Gdome in
  let notebook = (rendering_window ())#notebook in
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
+ let output = (rendering_window ())#output in
+ let outputhtml = (rendering_window ())#outputhtml in
   let metasenv =
    match ProofEngine.get_proof () with
       None -> assert false
@@ -890,11 +887,11 @@ let setgoal metano =
    with
       InvokeTactics.RefreshSequentException e ->
        output_html outputhtml
-        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-         "sequent: " ^ Printexc.to_string e ^ "</h1>")
+        (`Error (`T ("Exception raised during the refresh of the " ^
+         "sequent: " ^ Printexc.to_string e)))
     | e ->
        output_html outputhtml
-        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+        (`Error (`T (Printexc.to_string e)))
 ;;
 
 let
@@ -929,7 +926,7 @@ let
     with
      e ->
       output_html outputhtml
-       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+       (`Error (`T (Printexc.to_string e)))
   in
   let show_in_show_window_uri uri =
    let obj = CicEnvironment.get_obj uri in
@@ -981,10 +978,10 @@ let locate_callback id =
    (function uri,_ ->
      MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
    result in
-  out "<h1>Locate Query: </h1><pre>";
-  MQueryUtil.text_of_query out "" query; 
-  out "<h1>Result:</h1>";
-  MQueryUtil.text_of_result out "<br>" result;
+  out (`Msg (`T "Locate Query:")) ;
+  MQueryUtil.text_of_query (fun m -> out (`Msg (`T m))) "" query; 
+  out (`Msg (`T "Result:")) ;
+  MQueryUtil.text_of_result (fun m -> out (`Msg (`T m))) "" result;
   user_uri_choice ~title:"Ambiguous input."
    ~msg:
      ("Ambiguous input \"" ^ id ^
@@ -1040,21 +1037,21 @@ let input_or_locate_uri ~title =
    let uri = "cic:" ^ manual_input#text in
     try
       ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
-      output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
+      output_html outputhtml (`Msg (`T "OK")) ;
       true
     with
        Getter.Unresolved ->
         output_html outputhtml
-         ("<h1 color=\"Red\">URI " ^ uri ^
-          " does not correspond to any object.</h1>") ;
+         (`Error (`T ("URI " ^ uri ^
+          " does not correspond to any object."))) ;
         false
      | UriManager.IllFormedUri _ ->
         output_html outputhtml
-         ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
+         (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ;
         false
      | e ->
         output_html outputhtml
-         ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
+         (`Error (`T (Printexc.to_string e))) ;
         false
   in
   ignore
@@ -1113,7 +1110,7 @@ module Callbacks =
   let get_metasenv () = !ChosenTextualParser0.metasenv
   let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
 
-  let output_html msg = output_html (outputhtml ()) msg;;
+  let output_html msg = output_html (outputhtml ()) (`Msg (`T msg));;
   let interactive_user_uri_choice =
    fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
     interactive_user_uri_choice ~selection_mode ?ok
@@ -1141,7 +1138,7 @@ let locate () =
    with
     e ->
      output_html outputhtml
-      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+      (`Error (`T (Printexc.to_string e)))
 ;;
 
 
@@ -1250,7 +1247,7 @@ let new_inductive () =
        with
         e ->
          output_html outputhtml
-          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+          (`Error (`T (Printexc.to_string e)))
      ))
  (* Second phase *)
  and phase2 () =
@@ -1357,7 +1354,7 @@ let new_inductive () =
         with
          e ->
           output_html outputhtml
-           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+           (`Error (`T (Printexc.to_string e)))
       ))
  (* Third phase *)
  and phase3 name cons =
@@ -1431,7 +1428,7 @@ let new_inductive () =
        with
         e ->
          output_html outputhtml
-          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+          (`Error (`T (Printexc.to_string e)))
      )) ;
   window2#show () ;
   GtkThread.main ();
@@ -1477,7 +1474,7 @@ let new_inductive () =
    with
     e ->
      output_html outputhtml
-      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+      (`Error (`T (Printexc.to_string e)))
 ;;
 
 let new_proof () =
@@ -1576,7 +1573,7 @@ prerr_endline ("######################## " ^ xxx) ;
       with
        e ->
         output_html outputhtml
-         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+         (`Error (`T (Printexc.to_string e)))
   )) ;
  window#show () ;
  GtkThread.main ();
@@ -1597,15 +1594,15 @@ prerr_endline ("######################## " ^ xxx) ;
   with
      InvokeTactics.RefreshSequentException e ->
       output_html outputhtml
-       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-        "sequent: " ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e)))
    | InvokeTactics.RefreshProofException e ->
       output_html outputhtml
-       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-        "proof: " ^ Printexc.to_string e ^ "</h1>")
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e)))
    | e ->
       output_html outputhtml
-       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+       (`Error (`T (Printexc.to_string e)))
 ;;
 
 let check_term_in_scratch scratch_window metasenv context expr = 
@@ -1646,7 +1643,7 @@ let check scratch_window () =
    with
     e ->
      output_html outputhtml
-      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+      (`Error (`T (Printexc.to_string e)))
 ;;
 
 let show () =
@@ -1656,7 +1653,7 @@ let show () =
   with
    e ->
     output_html outputhtml
-     ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+     (`Error (`T (Printexc.to_string e)))
 ;;
 
 exception NotADefinition;;
@@ -1684,15 +1681,15 @@ let open_ () =
    with
       InvokeTactics.RefreshSequentException e ->
        output_html outputhtml
-        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-         "sequent: " ^ Printexc.to_string e ^ "</h1>")
+        (`Error (`T ("Exception raised during the refresh of the " ^
+         "sequent: " ^ Printexc.to_string e)))
     | InvokeTactics.RefreshProofException e ->
        output_html outputhtml
-        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-         "proof: " ^ Printexc.to_string e ^ "</h1>")
+        (`Error (`T ("Exception raised during the refresh of the " ^
+         "proof: " ^ Printexc.to_string e)))
     | e ->
        output_html outputhtml
-        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+        (`Error (`T (Printexc.to_string e)))
 ;;
 
 let show_query_results results =
@@ -1946,7 +1943,7 @@ let completeSearchPattern () =
   with
    e ->
     output_html outputhtml
-     ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+     (`Error (`T (Printexc.to_string e)))
 ;;
 
 let insertQuery () =
@@ -2014,7 +2011,7 @@ let insertQuery () =
   with
    e ->
     output_html outputhtml
-     ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+     (`Error (`T (Printexc.to_string e)))
 ;;
 
 let choose_must list_of_must only =
@@ -2157,8 +2154,8 @@ let searchPattern () =
          let uris' =
            TacticChaser.matchConclusion
 	    mqi_handle
-            ~output_html:(output_html outputhtml) ~choose_must ()
-            ~status:(proof, metano)
+            ~output_html:(fun m -> output_html outputhtml (`Msg (`T m)))
+            ~choose_must () ~status:(proof, metano)
          in
          let uri' =
           user_uri_choice ~title:"Ambiguous input."
@@ -2170,7 +2167,7 @@ let searchPattern () =
   with
    e -> 
     output_html outputhtml 
-     ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+     (`Error (`T (Printexc.to_string e)))
 ;;
       
 let choose_selection mmlwidget (element : Gdome.element option) =
@@ -2678,41 +2675,77 @@ end
 let dump_environment () =
   try
     let oc = open_out environmentfile in
-    output_html (outputhtml ()) "<b>Dumping environment ... </b><br />";
+    output_html (outputhtml ()) (`Msg (`T "Dumping environment ..."));
     CicEnvironment.dump_to_channel
-      ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+      ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
       oc;
-    output_html (outputhtml ()) "<b>... done!</b><br />";
+    output_html (outputhtml ()) (`Msg (`T "... done!")) ;
     close_out oc
   with exc ->
     output_html (outputhtml ())
-      (Printf.sprintf
+      (`Error (`T (Printf.sprintf
         "<h1 color=\"red\">Dump failure, uncaught exception:%s</h1>"
-        (Printexc.to_string exc))
+        (Printexc.to_string exc))))
 ;;
 let restore_environment () =
   try
     let ic = open_in environmentfile in
-    output_html (outputhtml ()) "<b>Restoring environment ... </b><br />";
+    output_html (outputhtml ()) (`Msg (`L [`T "Restoring environment ... " ; `BR]));
     CicEnvironment.restore_from_channel
-      ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+      ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`L [`T uri ; `BR])))
       ic;
-    output_html (outputhtml ()) "<b>... done!</b><br />";
+    output_html (outputhtml ()) (`Msg (`T "... done!"));
     close_in ic
   with exc ->
     output_html (outputhtml ())
-      (Printf.sprintf
+      (`Error (`T (Printf.sprintf
         "<h1 color=\"red\">Restore failure, uncaught exception:%s</h1>"
-        (Printexc.to_string exc))
+        (Printexc.to_string exc))))
 ;;
 
 (* HTML simulator (first in its kind) *)
 
-class fake_xmhtml ~source ~width ~height ~border_width ~packing ~show () =
- let tv = GText.view ~width ~height ~border_width ~packing ~show () in
+type log_msg =
+ [ `T of string
+ | `L of log_msg list 
+ | `BR
+ ]
+;;
+
+class logger ~width ~height ~packing ~show () =
+ let scrolled_window =
+  GBin.scrolled_window ~packing ~show () in
+ let vadj = scrolled_window#vadjustment in
+ let tv =
+  GText.view ~editable:false ~cursor_visible:false
+   ~width ~height ~packing:(scrolled_window#add) () in
+ let green =
+  tv#buffer#create_tag
+   [`FOREGROUND_SET true ;
+    `FOREGROUND_GDK
+     (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "green"))] in
+ let red =
+  tv#buffer#create_tag
+   [`FOREGROUND_SET true ;
+    `FOREGROUND_GDK
+     (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "red"))] in
   object
-   method set_topline (_:int) = ()
-   method source s = tv#buffer#insert s
+   method log (m : [`Msg of log_msg | `Error of log_msg]) =
+    let process_msg tags =
+     let rec aux =
+      function
+         `T s -> tv#buffer#insert ~tags s
+       | `L l -> List.iter aux l
+       | `BR -> tv#buffer#insert ~tags "\n"
+     in
+      aux
+    in
+     begin
+      match m with
+         `Msg m -> process_msg [green] m
+       | `Error m -> process_msg [red] m
+     end ;
+     vadj#set_value (vadj#upper)
   end
 ;;
 
@@ -2863,13 +2896,13 @@ class rendering_window output (notebook : notebook) =
         with
            InvokeTactics.RefreshSequentException e ->
             output_html (outputhtml ())
-             ("<h1 color=\"red\">An error occurred while refreshing the " ^
-               "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+             (`Error (`T ("An error occurred while refreshing the " ^
+               "sequent: " ^ Printexc.to_string e))) ;
            (*notebook#remove_all_pages ~skip_switch_page_event:false ;*)
            notebook#set_empty_page
          | InvokeTactics.RefreshProofException e ->
             output_html (outputhtml ())
-             ("<h1 color=\"red\">An error occurred while refreshing the proof: "               ^ Printexc.to_string e ^ "</h1>") ;
+             (`Error (`T ("An error occurred while refreshing the proof: "               ^ Printexc.to_string e))) ;
             output#unload
      ) in
  (* accel group *)
@@ -2906,13 +2939,8 @@ class rendering_window output (notebook : notebook) =
   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
  in
  let outputhtml =
-  new fake_xmhtml
-  (*
-  GHtml.xmhtml
-  *)
-   ~source:"<html><body bgColor=\"white\"></body></html>"
+  new logger
    ~width:400 ~height: 100
-   ~border_width:20
    ~packing:frame#add
    ~show:true () in
 object
@@ -2940,7 +2968,8 @@ object
   set_outputhtml outputhtml ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
   Logger.log_callback :=
-   (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
+   (Logger.log_to_html
+     ~print_and_flush:(fun m -> (output_html outputhtml (`Msg (`T m)))))
 end;;
 
 (* MAIN *)
@@ -2952,8 +2981,7 @@ let initialize_everything () =
    let rendering_window' = new rendering_window output notebook in
     set_rendering_window rendering_window' ;
     let print_error_as_html prefix msg =
-     output_html (outputhtml ())
-      ("<h1 color=\"red\">" ^ prefix ^ msg ^ "</h1>")
+     output_html (outputhtml ()) (`Error (`T (prefix ^ msg)))
     in
      Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
      Gdome_xslt.setDebugCallback