snapshot

[helm.git] / helm / matita / matitaConsole.ml

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 810914393549a720125bcfab14c8d51ab0e024d0..222055e6539a59b8b9ecfed8bf3434d746bcb936 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -70,6 +70,7 @@ class console
   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
   ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj
 =
+  let console_height = 100 in (* pixels *)
   object (self)
     inherit GText.view obj
 
@@ -143,10 +144,12 @@ class console
       history#add (* do not push trailing phrase separator *)
         (String.sub phrase 0
           (String.length phrase - String.length _phrase_sep));
-      if _callback phrase then
-        self#hide ()
+      if _callback phrase then begin
+        self#hide ();
+        self#clear ()
         (* else callback encountered troubles, don't hide console which
         probably contains error message *)
+      end
 
     method clear () =
       let buf = self#buffer in
@@ -183,13 +186,25 @@ class console
       self#ignore_insert_text_signal false;
       self#lock
 
+    method private get_paned_prop s =
+      Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int }
+        paned#as_widget
+    method private get_position = self#get_paned_prop "position"
+    method private get_min_position = self#get_paned_prop "min-position"
+    method private get_max_position = self#get_paned_prop "max-position"
+
     method show ?(msg = "") () =
       self#buffer#insert msg;
-      paned#set_position handle_position;
+      paned#set_position (self#get_max_position - console_height);
       self#misc#grab_focus ()
     method hide () =
-      self#clear ();
-      paned#set_position max_int
+      paned#set_position self#get_max_position
+    method toggle () =
+      let pos = self#get_position in
+      if pos > self#get_max_position - console_height then
+        self#show ()
+      else
+        self#hide ()
 
       (** navigation methods: history, cursor motion, ... *)
 
@@ -198,12 +213,18 @@ class console
     method private next_phrase =
       try self#set_phrase history#next with History_failure -> ()
 
-    method wrap_exn f =
+    method wrap_exn (f: unit -> unit) =
       try
-        f ()
-      with exn ->
-        self#echo_error (sprintf "Uncaught exception: %s"
-          (Printexc.to_string exn))
+        f ();
+        true
+      with
+      | StatefulProofEngine.Tactic_failure exn ->
+          self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn));
+          false
+      | exn ->
+          self#echo_error (sprintf "Uncaught exception: %s"
+            (Printexc.to_string exn));
+          false
 
   end