snapshot (notably: first working version of the console)

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

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index a2c0515bd05cc26efeed58bffbc955423e7b3df6..9c3c5a9b5aa7fb702ffa64f0d1e2e9695a91f7cf 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -33,12 +33,13 @@ let message_props = [ `STYLE `ITALIC ]
 let error_props = [ `WEIGHT `BOLD ]
 let prompt_props = [ ]
 
+let trailing_NL_RE = Pcre.regexp "\n\\s*$"
+
 class console
   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
   ?(callback = default_callback)
   obj
 =
-  let ui_mark = `NAME "USER_INPUT_START" in
   object (self)
     inherit GText.view obj
 
@@ -49,6 +50,10 @@ class console
     val mutable _callback = callback
     method set_callback f = _callback <- f
 
+    val mutable _ignore_insert_text_signal = false
+    method ignore_insert_text_signal ignore =
+      _ignore_insert_text_signal <- ignore
+
 (*
     (* TODO Zack: implement history.
        IDEA: use CTRL-P/N a la emacs.
@@ -60,49 +65,56 @@ class console
 
     initializer
       let buf = self#buffer in
+      self#set_wrap_mode `CHAR;
         (* create "USER_INPUT_START" mark. This mark will always point to the
         * beginning of user input not yet processed *)
       ignore (buf#create_mark ~name:"USER_INPUT_START"
         ~left_gravity:true buf#start_iter);
-      ignore (self#event#connect#key_press (fun key ->  (* handle return ev. *)
-        if GdkEvent.Key.keyval key = GdkKeysyms._Return then begin
-          let insert_point = buf#get_iter_at_mark `INSERT in
-          if insert_point#compare buf#end_iter = 0 then (* insert pt. at end *)
-            let inserted_text =
-              buf#get_text ~start:(buf#get_iter_at_mark ui_mark)
-                ~stop:buf#end_iter ()
-            in
-            let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
-            if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
-              self#lock;
-              _callback inserted_text
-            end
-        end;
-        false (* continue event processing *)))
+      ignore (buf#connect#after#insert_text (fun iter text ->
+        if (not _ignore_insert_text_signal) &&
+          (iter#compare buf#end_iter = 0) &&  (* insertion at end *)
+          (Pcre.pmatch ~rex:trailing_NL_RE text)
+        then
+          let inserted_text =
+            buf#get_text
+              ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
+              ~stop:buf#end_iter ()
+          in
+          let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
+          if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
+            self#lock;
+            _callback inserted_text;
+            self#echo_prompt ()
+          end))
 
       (* lock old text and bump USER_INPUT_START mark *)
     method private lock =
       let buf = self#buffer in
       let read_only = buf#create_tag [`EDITABLE false] in
-      let stop = buf#end_iter in
-      buf#apply_tag read_only ~start:buf#start_iter ~stop;
-      buf#move_mark ui_mark stop
+      buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter;
+      buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter
 
     method echo_prompt () =
       let buf = self#buffer in
+      self#ignore_insert_text_signal true;
       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt;
+      self#ignore_insert_text_signal false;
       self#lock
 
     method echo_message msg =
       let buf = self#buffer in
+      self#ignore_insert_text_signal true;
       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props]
         (msg ^ "\n");
+      self#ignore_insert_text_signal false;
       self#lock
 
     method echo_error msg =
       let buf = self#buffer in
+      self#ignore_insert_text_signal true;
       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
         (msg ^ "\n");
+      self#ignore_insert_text_signal false;
       self#lock
   end