snapshot (notably: implemented "check")

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

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 1f86e51a0c522aefdc68bc393ff7c7a6aec7fba4..5fb44adf486511c92067e5fd595c5c3cd0faa94e 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -27,8 +27,6 @@ let default_prompt = "# "
 let default_phrase_sep = "."
 let default_callback = fun (phrase: string) -> ()
 
-let history_size = 100
-
 let message_props = [ `STYLE `ITALIC ]
 let error_props = [ `WEIGHT `BOLD ]
 let prompt_props = [ ]
@@ -85,7 +83,7 @@ class console
     method ignore_insert_text_signal ignore =
       _ignore_insert_text_signal <- ignore
 
-    val history = new history history_size
+    val history = new history BuildTimeConf.console_history_size
 
     initializer
       let buf = self#buffer in
@@ -110,17 +108,21 @@ class console
             self#invoke_callback inserted_text;
             self#echo_prompt ()
           end));
-      (match evbox with
+      (match evbox with (* history key bindings *)
       | None -> ()
       | Some evbox ->
           List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox)
             [ GdkKeysyms._p, (fun () -> self#previous_phrase);
               GdkKeysyms._n, (fun () -> self#next_phrase);
-              GdkKeysyms._a, (fun () -> self#beginning_of_phrase);
-              GdkKeysyms._e, (fun () -> self#end_of_phrase);
-              GdkKeysyms._f, (fun () -> self#forward_char);
-              GdkKeysyms._b, (fun () -> self#backward_char);
-            ])
+            ]);
+      ignore (self#connect#after#move_cursor
+        (* avoid cursor being placed at prompt's left *)
+        ~callback:(fun step count ~extend ->
+            let buf = self#buffer in
+            let cursor_iter = buf#get_iter_at_mark `INSERT in
+            let prompt_iter = buf#get_iter_at_mark (`NAME "USER_INPUT_START") in
+            if prompt_iter#compare cursor_iter = 1 then (* prompt > cursor *)
+              buf#place_cursor ~where:prompt_iter))
 
     method private set_phrase phrase =
       let buf = self#buffer in
@@ -171,18 +173,6 @@ class console
       try self#set_phrase history#previous with History_failure -> ()
     method private next_phrase =
       try self#set_phrase history#next with History_failure -> ()
-    method private beginning_of_phrase =
-      let buf = self#buffer in
-      buf#place_cursor ~where:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
-    method private end_of_phrase =
-      let buf = self#buffer in
-      buf#place_cursor ~where:buf#end_iter
-    method private forward_char =
-      let buf = self#buffer in
-      buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#forward_char
-    method private backward_char =
-      let buf = self#buffer in
-      buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#backward_char
 
   end