X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.ml;h=8dc43a093d3ba5f77205db126af45daf40499833;hb=81ad82070892b2f2740111d97b2d72394f969328;hp=3d40e949ee46ae156abe5e34625c7dbac8346fc2;hpb=d0991ea0c7c83c100b2d223644cb2f11a8554fa1;p=helm.git

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 3d40e949e..8dc43a093 100644
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -29,8 +29,7 @@ open MatitaTypes
 
 type callback = string -> command_outcome
 
-(* let default_prompt = "# " *)
-let default_prompt = ""
+let default_prompt = "# "
 let default_phrase_sep = "."
 let default_callback = fun (phrase: string) -> (true, true)
 let bullet = "∙"
@@ -41,34 +40,6 @@ let prompt_props = [ ]
 
 let trailing_NL_RE = Pcre.regexp "\n\\s*$"
 
-exception History_failure
-
-  (** shell like phrase history *)
-class history size =
-  let size = size + 1 in
-  let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
-  let incr x = (x + 1) mod size in
-  object
-    val data = Array.create size ""
-    val mutable hd = 0  (* insertion point *)
-    val mutable tl = -1 (* oldest inserted item *)
-    val mutable cur = -1  (* current item for the history *)
-    method add s =
-      data.(hd) <- s;
-      if tl = -1 then tl <- hd;
-      hd <- incr hd;
-      if hd = tl then tl <- incr tl;
-      cur <- hd
-    method previous =
-      if cur = tl then raise History_failure;
-      cur <- decr cur;
-      data.(cur)
-    method next =
-      if cur = hd then raise History_failure;
-      cur <- incr cur;
-      if cur = hd then "" else data.(cur)
-  end
-
 class console
   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
   ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj
@@ -92,7 +63,8 @@ class console
     method ignore_insert_text_signal ignore =
       _ignore_insert_text_signal <- ignore
 
-    val history = new history BuildTimeConf.console_history_size
+    val history =
+      new MatitaMisc.shell_history BuildTimeConf.console_history_size
 
     val mutable handle_position = 450
     val mutable last_phrase = ""
@@ -105,6 +77,22 @@ class console
         * beginning of user input not yet processed *)
       ignore (buf#create_mark ~name:"USER_INPUT_START"
         ~left_gravity:true buf#start_iter);
+      MatitaGtkMisc.connect_key self#event ~modifiers:[`CONTROL] ~stop:true
+        GdkKeysyms._Return
+        (fun () ->
+          buf#insert ~iter:buf#end_iter "\n";
+          let inserted_text =
+            MatitaMisc.strip_trailing_blanks
+              (buf#get_text
+                ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
+                ~stop:buf#end_iter ())
+          in
+          self#invoke_callback inserted_text;
+          self#echo_prompt ());
+
+(*
+      (* callback handling based on phrase terminator (e.g. ";;" at the end of
+      * the row: each time a character is inserted *)
       ignore (buf#connect#after#insert_text (fun iter text ->
         if (not _ignore_insert_text_signal) &&
           (iter#compare buf#end_iter = 0) &&  (* insertion at end *)
@@ -123,6 +111,7 @@ class console
             self#invoke_callback inserted_text;
             self#echo_prompt ()
           end));
+*)
       (match evbox with (* history key bindings *)
       | None -> ()
       | Some evbox ->
@@ -212,9 +201,9 @@ class console
       (** navigation methods: history, cursor motion, ... *)
 
     method private previous_phrase =
-      try self#set_phrase history#previous with History_failure -> ()
+      try self#set_phrase history#previous with MatitaMisc.History_failure -> ()
     method private next_phrase =
-      try self#set_phrase history#next with History_failure -> ()
+      try self#set_phrase history#next with MatitaMisc.History_failure -> ()
 
     method wrap_exn: 'a. (unit -> 'a) -> 'a option =
       fun f ->