From ee35ccaff9728ecba44c83eed9cb703d9a1f131e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 16 Dec 2003 15:59:54 +0000 Subject: [PATCH] - fixed logging in log window so that spurious html tags are no longer printed - factorized a lot of error handling code in invokeTactics - moved (and reimplemented) logger class to ui_logger module --- helm/gTopLevel/.depend | 19 +- helm/gTopLevel/Makefile | 2 +- helm/gTopLevel/disambiguate.ml | 20 +- helm/gTopLevel/disambiguate.mli | 2 +- helm/gTopLevel/gTopLevel.ml | 102 ++-------- helm/gTopLevel/invokeTactics.ml | 335 ++++++++++--------------------- helm/gTopLevel/invokeTactics.mli | 2 +- helm/gTopLevel/ui_logger.ml | 76 +++++++ helm/gTopLevel/ui_logger.mli | 19 ++ 9 files changed, 251 insertions(+), 326 deletions(-) create mode 100644 helm/gTopLevel/ui_logger.ml create mode 100644 helm/gTopLevel/ui_logger.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index e7f7c2d1d..af4bb9a3c 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,13 +1,14 @@ +disambiguate.cmi: ui_logger.cmi termEditor.cmi: disambiguate.cmi texTermEditor.cmi: disambiguate.cmi -invokeTactics.cmi: termEditor.cmi termViewer.cmi +invokeTactics.cmi: termEditor.cmi termViewer.cmi ui_logger.cmi hbugs.cmi: invokeTactics.cmi proofEngine.cmo: proofEngine.cmi proofEngine.cmx: proofEngine.cmi logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi -disambiguate.cmo: disambiguate.cmi -disambiguate.cmx: disambiguate.cmi +disambiguate.cmo: ui_logger.cmi disambiguate.cmi +disambiguate.cmx: ui_logger.cmx disambiguate.cmi termEditor.cmo: disambiguate.cmi termEditor.cmi termEditor.cmx: disambiguate.cmx termEditor.cmi texTermEditor.cmo: disambiguate.cmi texTermEditor.cmi @@ -17,12 +18,16 @@ xmlDiff.cmx: xmlDiff.cmi termViewer.cmo: logicalOperations.cmi xmlDiff.cmi termViewer.cmi termViewer.cmx: logicalOperations.cmx xmlDiff.cmx termViewer.cmi invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \ - termViewer.cmi invokeTactics.cmi + termViewer.cmi ui_logger.cmi invokeTactics.cmi invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \ - termViewer.cmx invokeTactics.cmi + termViewer.cmx ui_logger.cmx invokeTactics.cmi hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi +ui_logger.cmo: ui_logger.cmi +ui_logger.cmx: ui_logger.cmi gTopLevel.cmo: hbugs.cmi invokeTactics.cmi logicalOperations.cmi \ - proofEngine.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi + proofEngine.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi \ + ui_logger.cmi gTopLevel.cmx: hbugs.cmx invokeTactics.cmx logicalOperations.cmx \ - proofEngine.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx + proofEngine.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx \ + ui_logger.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 7ce96c052..437e41c21 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -25,7 +25,7 @@ stop: INTERFACE_FILES = \ proofEngine.mli logicalOperations.mli disambiguate.mli \ termEditor.mli texTermEditor.mli xmlDiff.mli termViewer.mli \ - invokeTactics.mli hbugs.mli + invokeTactics.mli hbugs.mli ui_logger.mli DEPOBJS = $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index efb1c0508..07a036839 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -33,6 +33,8 @@ (* *) (******************************************************************************) +open Printf + (** This module provides a functor to disambiguate the input **) (** given a set of user-interface call-backs **) @@ -44,7 +46,7 @@ module type Callbacks = val get_metasenv : unit -> Cic.metasenv val set_metasenv : Cic.metasenv -> unit - val output_html : string -> unit + val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit val interactive_user_uri_choice : selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> @@ -72,10 +74,12 @@ module Make(C:Callbacks) = (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri ) result in - C.output_html "

Locate Query: 

";
-     MQueryUtil.text_of_query C.output_html "" query; 
-     C.output_html "
Result:
";
-     MQueryUtil.text_of_result C.output_html "
" result;
+     C.output_html (`Msg (`T "Locate query:"));
+     MQueryUtil.text_of_query
+      (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
+      "" query; 
+     C.output_html (`Msg (`T "Result:"));
+     MQueryUtil.text_of_result (fun s -> C.output_html (`Msg (`T s))) "" result;
      let uris' =
       match uris with
          [] ->
@@ -142,9 +146,9 @@ module Make(C:Callbacks) =
        ) 1 list_of_uris
      in
       if tests_no > 1 then
-       C.output_html
-        ("
Disambiguation phase started: up to " ^
-          string_of_int tests_no ^ " cases will be tried.") ;
+       C.output_html (`Msg (`T (sprintf
+        "Disambiguation phase started: up to %d cases will be tried"
+        tests_no)));
      (* and now we compute the list of all possible assignments from *)
      (* id to uris that generate well-typed terms                    *)
      let resolve_ids =
diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli
index 0114ce27f..79e77df48 100644
--- a/helm/gTopLevel/disambiguate.mli
+++ b/helm/gTopLevel/disambiguate.mli
@@ -44,7 +44,7 @@ module type Callbacks =
     val get_metasenv : unit -> Cic.metasenv
     val set_metasenv : Cic.metasenv -> unit
 
-    val output_html : string -> unit
+    val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
     val interactive_user_uri_choice :
       selection_mode:[`SINGLE | `MULTIPLE] ->
       ?ok:string ->
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 8aec9d350..fa1ad6ea8 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -53,16 +53,6 @@ let mqi_handle = MQIC.init mqi_flags prerr_string
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
-let htmlheader =
- "" ^
- " "
-;;
-
-let htmlfooter =
- " " ^
- ""
-;;
-
 let prooffile =
  try
   Sys.getenv "GTOPLEVEL_PROOFFILE"
@@ -89,8 +79,6 @@ let notify_hbugs_on_goal_change = false ;;
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
-let htmlheader_and_content = ref htmlheader;;
-
 let check_term = ref (fun _ _ _ -> assert false);;
 
 exception RenderingWindowsNotInitialized;;
@@ -121,11 +109,11 @@ exception OutputHtmlNotInitialized;;
 
 let set_outputhtml,outputhtml =
  let outputhtml_ref = ref None in
-  (function rw -> outputhtml_ref := Some rw),
+  (function (rw: Ui_logger.html_logger) -> outputhtml_ref := Some rw),
   (function () ->
     match !outputhtml_ref with
-       None -> raise OutputHtmlNotInitialized
-     | Some outputhtml -> outputhtml
+     | None -> raise OutputHtmlNotInitialized
+     | Some outputhtml -> (outputhtml: Ui_logger.html_logger)
   )
 ;;
 
@@ -179,15 +167,14 @@ let string_of_cic_textual_parser_uri uri =
    String.sub uri' 4 (String.length uri' - 4)
 ;;
 
-let output_html outputhtml msg =
- outputhtml#log msg
-;;
+let output_html ?(append_NL = true) (outputhtml: Ui_logger.html_logger) =
+  outputhtml#log ~append_NL
 
 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
 
 (* Check window *)
 
-let check_window outputhtml uris =
+let check_window (outputhtml: Ui_logger.html_logger) uris =
  let window =
   GWindow.window
    ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
@@ -218,8 +205,7 @@ let check_window outputhtml uris =
           mmlwidget#load_sequent [] (111,[],expr)
          with
           e ->
-           output_html outputhtml
-            (`Error (`T (Printexc.to_string e)))
+           output_html outputhtml (`Error (`T (Printexc.to_string e)))
        )
    ) uris
  in
@@ -668,7 +654,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 (`T msg))
+  let output_html msg = output_html (outputhtml ()) msg
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
@@ -1108,13 +1094,13 @@ module Callbacks =
   let get_metasenv () = !ChosenTextualParser0.metasenv
   let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
 
-  let output_html msg = output_html (outputhtml ()) (`Msg (`T msg));;
+  let output_html ?append_NL = output_html ?append_NL (outputhtml ())
   let interactive_user_uri_choice =
    fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
     interactive_user_uri_choice ~selection_mode ?ok
-     ?enable_button_for_non_vars ~title ~msg;;
-  let interactive_interpretation_choice = interactive_interpretation_choice;;
-  let input_or_locate_uri = input_or_locate_uri;;
+     ?enable_button_for_non_vars ~title ~msg
+  let interactive_interpretation_choice = interactive_interpretation_choice
+  let input_or_locate_uri = input_or_locate_uri
  end
 ;;
 
@@ -2681,72 +2667,24 @@ let dump_environment () =
     close_out oc
   with exc ->
     output_html (outputhtml ())
-      (`Error (`T (Printf.sprintf
-        "
Dump failure, uncaught exception:%s
"
+      (`Error (`T (Printf.sprintf "Dump failure, uncaught exception:%s"
         (Printexc.to_string exc))))
 ;;
 let restore_environment () =
   try
     let ic = open_in environmentfile in
-    output_html (outputhtml ()) (`Msg (`L [`T "Restoring environment ... " ; `BR]));
+    output_html (outputhtml ()) (`Msg (`T "Restoring environment ... "));
     CicEnvironment.restore_from_channel
-      ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`L [`T uri ; `BR])))
+      ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
       ic;
     output_html (outputhtml ()) (`Msg (`T "... done!"));
     close_in ic
   with exc ->
     output_html (outputhtml ())
-      (`Error (`T (Printf.sprintf
-        "
Restore failure, uncaught exception:%s
"
+      (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s"
         (Printexc.to_string exc))))
 ;;
 
-(* HTML simulator (first in its kind) *)
-
-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 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
-;;
-
 (* Main window *)
 
 class rendering_window output (notebook : notebook) =
@@ -2937,7 +2875,7 @@ class rendering_window output (notebook : notebook) =
   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
  in
  let outputhtml =
-  new logger
+  new Ui_logger.html_logger
    ~width:400 ~height: 100
    ~packing:frame#add
    ~show:true () in
@@ -2965,10 +2903,8 @@ object
   set_settings_window settings_window ;
   set_outputhtml outputhtml ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
-  Logger.log_callback :=
-   (Logger.log_to_html
-     ~print_and_flush:(fun m -> (output_html outputhtml (`Msg (`T m)))))
-end;;
+  CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true)
+end
 
 (* MAIN *)
 
diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 79b489f54..e4a9fa2e9 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -33,6 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
+open Printf
+
 exception RefreshSequentException of exn;;
 exception RefreshProofException of exn;;
 
@@ -52,7 +54,7 @@ module type Callbacks =
         context: Cic.context ;
         set_context : Cic.context -> unit >
     (* output messages *)
-    val output_html : string -> unit
+    val output_html : Ui_logger.html_msg -> unit
     (* GUI refresh functions *)
     val refresh_proof : unit -> unit
     val refresh_goals : unit -> unit
@@ -110,36 +112,43 @@ module type Tactics =
 module Make (C: Callbacks) : Tactics =
   struct
 
+   let print_uncaught_exception e =
+     C.output_html (`Error (`T (sprintf "Uncaught exception: %s"
+      (Printexc.to_string e))))
+
+   let handle_refresh_exception f savedproof savedgoal =
+     try
+       f ()
+     with
+     | RefreshSequentException e ->
+        C.output_html (`Error (`T
+          (sprintf "Exception raised during the refresh of the sequent: %s"
+            (Printexc.to_string e))));
+        ProofEngine.set_proof savedproof ;
+        ProofEngine.goal := savedgoal ;
+        C.refresh_goals ()
+     | RefreshProofException e ->
+        C.output_html (`Error (`T
+          (sprintf "Exception raised during the refresh of the proof: %s"
+            (Printexc.to_string e))));
+        ProofEngine.set_proof savedproof ;
+        ProofEngine.goal := savedgoal ;
+        C.refresh_goals () ;
+        C.refresh_proof ()
+     | e ->
+        print_uncaught_exception e;
+        ProofEngine.set_proof savedproof ;
+        ProofEngine.goal := savedgoal
+
    let call_tactic tactic () =
     let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
-     begin
-      try
-       tactic () ;
-       C.refresh_goals () ;
-       C.refresh_proof ()
-      with
-         RefreshSequentException e ->
-          C.output_html
-           ("
Exception raised during the refresh of the " ^
-            "sequent: " ^ Printexc.to_string e ^ "
") ;
-          ProofEngine.set_proof savedproof ;
-          ProofEngine.goal := savedgoal ;
-          C.refresh_goals ()
-       | RefreshProofException e ->
-          C.output_html
-           ("
Exception raised during the refresh of the " ^
-            "proof: " ^ Printexc.to_string e ^ "
") ;
-          ProofEngine.set_proof savedproof ;
-          ProofEngine.goal := savedgoal ;
-          C.refresh_goals () ;
-          C.refresh_proof ()
-       | e ->
-          C.output_html
-           ("
" ^ Printexc.to_string e ^ "
") ;
-          ProofEngine.set_proof savedproof ;
-          ProofEngine.goal := savedgoal
-     end
+    handle_refresh_exception
+      (fun () ->
+        tactic ();
+        C.refresh_goals ();
+        C.refresh_proof ())
+      savedproof savedgoal
 
    let call_tactic_with_input tactic ?term () =
     let savedproof = ProofEngine.get_proof () in
@@ -158,39 +167,20 @@ module Make (C: Callbacks) : Tactics =
            in
             canonical_context
       in
-       try
-        let metasenv',expr =
-         (match term with
-         | None -> ()
-         | Some t -> (C.term_editor ())#set_term t);
-         (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
-        in
-         ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
-         tactic expr ;
-         C.refresh_goals () ;
-         C.refresh_proof () ;
-         (C.term_editor ())#reset
-       with
-          RefreshSequentException e ->
-           C.output_html
-            ("
Exception raised during the refresh of the " ^
-             "sequent: " ^ Printexc.to_string e ^ "
") ;
-           ProofEngine.set_proof savedproof ;
-           ProofEngine.goal := savedgoal ;
-           C.refresh_goals ()
-        | RefreshProofException e ->
-           C.output_html
-            ("
Exception raised during the refresh of the " ^
-             "proof: " ^ Printexc.to_string e ^ "
") ;
-           ProofEngine.set_proof savedproof ;
-           ProofEngine.goal := savedgoal ;
+       handle_refresh_exception
+        (fun () ->
+          let metasenv',expr =
+           (match term with
+           | None -> ()
+           | Some t -> (C.term_editor ())#set_term t);
+           (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
+          in
+           ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+           tactic expr ;
            C.refresh_goals () ;
-           C.refresh_proof ()
-        | e ->
-           C.output_html
-            ("
" ^ Printexc.to_string e ^ "
") ;
-           ProofEngine.set_proof savedproof ;
-           ProofEngine.goal := savedgoal
+           C.refresh_proof () ;
+           (C.term_editor ())#reset)
+        savedproof savedgoal
 
   let call_tactic_with_goal_input tactic () =
    let module L = LogicalOperations in
@@ -198,76 +188,30 @@ module Make (C: Callbacks) : Tactics =
     let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_terms with
-       [term] ->
-         begin
-          try
-           tactic term ;
-           C.refresh_goals () ;
-           C.refresh_proof ()
-          with
-             RefreshSequentException e ->
-              C.output_html
-               ("
Exception raised during the refresh of " ^
-                "the sequent: " ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals ()
-           | RefreshProofException e ->
-              C.output_html
-               ("
Exception raised during the refresh of " ^
-                "the proof: " ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals () ;
-              C.refresh_proof ()
-           | e ->
-              C.output_html
-               ("
" ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-         end
-     | [] ->
-        C.output_html
-         ("
No term selected
")
-     | _ ->
-        C.output_html
-         ("
Many terms selected
")
+     | [term] ->
+         handle_refresh_exception
+          (fun () ->
+            tactic term ;
+            C.refresh_goals () ;
+            C.refresh_proof ())
+          savedproof savedgoal
+     | [] -> C.output_html (`Error (`T "No term selected"))
+     | _ -> C.output_html (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_inputs tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
     let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
-     try
-      match (C.sequent_viewer ())#get_selected_terms with
-         [] ->
-          C.output_html
-           ("
No term selected
")
-       | terms ->
-          tactic terms ;
-          C.refresh_goals () ;
-          C.refresh_proof () ;
-     with
-        RefreshSequentException e ->
-         C.output_html
-          ("
Exception raised during the refresh of the " ^
-           "sequent: " ^ Printexc.to_string e ^ "
") ;
-         ProofEngine.set_proof savedproof ;
-         ProofEngine.goal := savedgoal ;
-         C.refresh_goals ()
-      | RefreshProofException e ->
-         C.output_html
-          ("
Exception raised during the refresh of the " ^
-           "proof: " ^ Printexc.to_string e ^ "
") ;
-         ProofEngine.set_proof savedproof ;
-         ProofEngine.goal := savedgoal ;
-         C.refresh_goals () ;
-         C.refresh_proof ()
-      | e ->
-         C.output_html
-          ("
" ^ Printexc.to_string e ^ "
") ;
-         ProofEngine.set_proof savedproof ;
-         ProofEngine.goal := savedgoal
+     handle_refresh_exception
+      (fun () ->
+        match (C.sequent_viewer ())#get_selected_terms with
+         | [] -> C.output_html (`Error (`T "No term selected"))
+         | terms ->
+            tactic terms ;
+            C.refresh_goals () ;
+            C.refresh_proof ())
+      savedproof savedgoal
 
   let call_tactic_with_input_and_goal_input tactic () =
    let module L = LogicalOperations in
@@ -276,64 +220,40 @@ module Make (C: Callbacks) : Tactics =
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_terms with
        [term] ->
-         begin
-          try
-           let uri,metasenv,bo,ty =
-            match ProofEngine.get_proof () with
-               None -> assert false
-             | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
-           in
-            let canonical_context =
-             match !ProofEngine.goal with
-                None -> assert false
-              | Some metano ->
-                 let (_,canonical_context,_) =
-                  List.find (function (m,_,_) -> m=metano) metasenv
-                 in
-                  canonical_context in
-            let (metasenv',expr) =
-             (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
-            in
-             ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
-             tactic ~goal_input:term ~input:expr ;
-             C.refresh_goals () ;
-             C.refresh_proof () ;
-             (C.term_editor ())#reset
-          with
-             RefreshSequentException e ->
-              C.output_html
-               ("
Exception raised during the refresh of " ^
-                "the sequent: " ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals ()
-           | RefreshProofException e ->
-              C.output_html
-               ("
Exception raised during the refresh of " ^
-                "the proof: " ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals () ;
-              C.refresh_proof ()
-           | e ->
-              C.output_html
-               ("
" ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-         end
-     | [] ->
-        C.output_html
-         ("
No term selected
")
-     | _ ->
-        C.output_html
-         ("
Many terms selected
")
+         handle_refresh_exception
+          (fun () ->
+             let uri,metasenv,bo,ty =
+              match ProofEngine.get_proof () with
+                 None -> assert false
+               | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+             in
+              let canonical_context =
+               match !ProofEngine.goal with
+                  None -> assert false
+                | Some metano ->
+                   let (_,canonical_context,_) =
+                    List.find (function (m,_,_) -> m=metano) metasenv
+                   in
+                    canonical_context in
+              let (metasenv',expr) =
+               (C.term_editor ())#get_metasenv_and_term
+                canonical_context metasenv
+              in
+               ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+               tactic ~goal_input:term ~input:expr ;
+               C.refresh_goals () ;
+               C.refresh_proof () ;
+               (C.term_editor ())#reset)
+          savedproof savedgoal
+     | [] -> C.output_html (`Error (`T "No term selected"))
+     | _ -> C.output_html (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_input_in_scratch tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
     let scratch_window = C.scratch_window () in
      match scratch_window#sequent_viewer#get_selected_terms with
-       [term] ->
+     | [term] ->
          begin
           try
            let expr = tactic term scratch_window#term in
@@ -342,25 +262,17 @@ module Make (C: Callbacks) : Tactics =
             scratch_window#set_term expr ;
             scratch_window#show () ;
           with
-           e ->
-            C.output_html
-             ("
" ^ Printexc.to_string e ^ "
")
+           e -> print_uncaught_exception e
          end
-     | [] ->
-        C.output_html
-         ("
No term selected
")
-     | _ ->
-        C.output_html
-         ("
Many terms selected
")
+     | [] -> C.output_html (`Error (`T "No term selected"))
+     | _ -> C.output_html (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_inputs_in_scratch tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
     let scratch_window = C.scratch_window () in
      match scratch_window#sequent_viewer#get_selected_terms with
-        [] ->
-         C.output_html
-          ("
No terms selected
")
+      | [] -> C.output_html (`Error (`T "No term selected"))
       | terms ->
          try
           let expr = tactic terms scratch_window#term in
@@ -369,9 +281,7 @@ module Make (C: Callbacks) : Tactics =
            scratch_window#set_term expr ;
            scratch_window#show () ;
          with
-          e ->
-           C.output_html
-            ("
" ^ Printexc.to_string e ^ "
")
+          e -> print_uncaught_exception e
 
   let call_tactic_with_hypothesis_input tactic () =
    let module L = LogicalOperations in
@@ -379,40 +289,15 @@ module Make (C: Callbacks) : Tactics =
     let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_hypotheses with
-       [hypothesis] ->
-         begin
-          try
-           tactic hypothesis ;
-           C.refresh_goals () ;
-           C.refresh_proof ()
-          with
-             RefreshSequentException e ->
-              C.output_html
-               ("
Exception raised during the refresh of " ^
-                "the sequent: " ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals ()
-           | RefreshProofException e ->
-              C.output_html
-               ("
Exception raised during the refresh of " ^
-                "the proof: " ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals () ;
-              C.refresh_proof ()
-           | e ->
-              C.output_html
-               ("
" ^ Printexc.to_string e ^ "
") ;
-              ProofEngine.set_proof savedproof ;
-              ProofEngine.goal := savedgoal ;
-         end
-     | [] ->
-        C.output_html
-         ("
No hypothesis selected
")
-     | _ ->
-        C.output_html
-         ("
Many hypothesis selected
")
+     | [hypothesis] ->
+         handle_refresh_exception
+           (fun () ->
+             tactic hypothesis ;
+             C.refresh_goals () ;
+             C.refresh_proof ())
+           savedproof savedgoal
+     | [] -> C.output_html (`Error (`T "No hypothesis selected"))
+     | _ -> C.output_html (`Error (`T "Too many hypotheses selected"))
 
 
   let intros =
diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 2c11fb3d3..200e50a15 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -52,7 +52,7 @@ module type Callbacks =
         context: Cic.context ;
         set_context : Cic.context -> unit >
     (* output messages *)
-    val output_html : string -> unit
+    val output_html : Ui_logger.html_msg -> unit
     (* GUI refresh functions *)
     val refresh_proof : unit -> unit
     val refresh_goals : unit -> unit
diff --git a/helm/gTopLevel/ui_logger.ml b/helm/gTopLevel/ui_logger.ml
new file mode 100644
index 000000000..019748613
--- /dev/null
+++ b/helm/gTopLevel/ui_logger.ml
@@ -0,0 +1,76 @@
+
+open Printf
+
+(* HTML simulator (first in its kind) *)
+
+type html_tag =
+ [ `T of string
+ | `L of html_tag list 
+ | `BR
+ ]
+
+type html_msg = [ `Error of html_tag | `Msg of html_tag ]
+
+class html_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 (self)
+
+   method log ?(append_NL = true)
+    (m : [`Msg of html_tag | `Error of html_tag])
+   =
+    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
+    (match m with
+     | `Msg m -> process_msg [green] m
+     | `Error m -> process_msg [red] m);
+    if append_NL then
+      process_msg [] `BR;
+    vadj#set_value (vadj#upper)
+
+   val mutable cic_indent_level = 0
+
+   method log_cic_msg ?(append_NL = true) (cic_msg: CicLogger.msg) =
+     let get_indent () = String.make cic_indent_level ' ' in
+     let incr () = cic_indent_level <- cic_indent_level + 1 in
+     let decr () = cic_indent_level <- cic_indent_level - 1 in
+     let msg =
+       get_indent () ^
+       (match cic_msg with
+       | `Start_type_checking uri ->
+           incr ();
+           sprintf "Type checking of %s started" (UriManager.string_of_uri uri)
+       | `Type_checking_completed uri ->
+           decr ();
+           sprintf "Type checking of %s completed"
+            (UriManager.string_of_uri uri)
+       | `Trusting uri ->
+           sprintf "%s is trusted" (UriManager.string_of_uri uri))
+     in
+     self#log ~append_NL (`Msg (`T msg))
+
+  end
+
diff --git a/helm/gTopLevel/ui_logger.mli b/helm/gTopLevel/ui_logger.mli
new file mode 100644
index 000000000..a289e370e
--- /dev/null
+++ b/helm/gTopLevel/ui_logger.mli
@@ -0,0 +1,19 @@
+
+type html_tag = [ `BR | `L of html_tag list | `T of string ]
+type html_msg = [ `Error of html_tag | `Msg of html_tag ]
+
+class html_logger:
+  width:int -> height:int ->
+  packing:(GObj.widget -> unit) -> show:bool ->
+  unit ->
+  object
+      (* in all methods below "append_NL" defaults to true *)
+
+      (** log an HTML like message, see minimal markup above *)
+    method log: ?append_NL:bool -> html_msg -> unit
+
+      (** log a cic messages as degined in CicLogger *)
+    method log_cic_msg: ?append_NL:bool -> CicLogger.msg -> unit
+
+  end
+
-- 
2.39.2