renamed Http_client to Http_user_agent to avoid clashes with Gerd's

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

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 1f86e51a0c522aefdc68bc393ff7c7a6aec7fba4..603a480f45553392920cf27e3c67a031b1d80453 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
@@ -163,7 +165,8 @@ class console
       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
         (msg ^ "\n");
       self#ignore_insert_text_signal false;
-      self#lock
+      self#lock;
+      self#echo_prompt ()
 
       (** navigation methods: history, cursor motion, ... *)
 
@@ -171,18 +174,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