snapshot

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 017f3955512668b579b8834c2f7a938e359b4b38..6ad3e81e0c015e57c1ff40e83a6c283a0c14c904 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -54,6 +54,12 @@ class gui file =
   let keyBindingBoxes = (* event boxes which should receive global key events *)
     [ toolbar#toolBarEventBox; proof#proofWinEventBox ]
   in
+  let console = MatitaConsole.console ~packing:main#scrolledConsole#add () in
+  let _ =
+    console#echo_message "message";
+    console#echo_error "error";
+    console#echo_prompt ()
+  in
   object (self)
     initializer
         (* glade's check widgets *)
@@ -102,8 +108,8 @@ class gui file =
       dialog#check_widgets ();
       dialog
 
-    method newTextDialog () =
-      let dialog = new textDialog ~file () in
+    method newEmptyDialog () =
+      let dialog = new emptyDialog ~file () in
       dialog#check_widgets ();
       dialog