X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.ml;h=8dc43a093d3ba5f77205db126af45daf40499833;hb=2026624f827b29c35d54aa67b301250123ea7311;hp=4735fdd4a8e0d5533ddca47778b3ced323ff0295;hpb=c4afa186c53998a10eab85d3fcc113b07bccfdf9;p=helm.git

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 4735fdd4a..8dc43a093 100644
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -27,10 +27,11 @@ open Printf
 
 open MatitaTypes
 
-(* let default_prompt = "# " *)
-let default_prompt = ""
+type callback = string -> command_outcome
+
+let default_prompt = "# "
 let default_phrase_sep = "."
-let default_callback = fun (phrase: string) -> true
+let default_callback = fun (phrase: string) -> (true, true)
 let bullet = "∙"
 
 let message_props = [ `STYLE `ITALIC ]
@@ -39,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
@@ -90,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 = ""
@@ -103,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 *)
@@ -121,6 +111,7 @@ class console
             self#invoke_callback inserted_text;
             self#echo_prompt ()
           end));
+*)
       (match evbox with (* history key bindings *)
       | None -> ()
       | Some evbox ->
@@ -146,12 +137,8 @@ class console
 
     method private invoke_callback phrase =
       history#add phrase;
-      if _callback phrase then begin
-        self#hide ();
-        self#clear ()
-      end
-        (* else callback encountered troubles, don't hide console which
-        probably contains error message *)
+      let (success, hide) = _callback phrase in
+      if hide then self#hide ()
 
     method clear () =
       let buf = self#buffer in
@@ -200,8 +187,10 @@ class console
       self#buffer#insert msg;
       paned#set_position (self#get_max_position - console_height);
       self#misc#grab_focus ()
-    method hide () =
-      paned#set_position self#get_max_position
+    method hide () =  (* ZACK still not sure about the gui, for the moment just
+                       * keep the console persistent *)
+      ()
+(*       paned#set_position self#get_max_position *)
     method toggle () =
       let pos = self#get_position in
       if pos > self#get_max_position - console_height then
@@ -212,37 +201,32 @@ 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 -> ()
-
-    method wrap_exn (f: unit -> unit) =
-      try
-        f ();
-        true
-      with
-      | StatefulProofEngine.Tactic_failure exn ->
-          self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn));
-          false
-      | CicTextualParser2.Parse_error (floc, msg) ->
-          let buf = self#buffer in
-          let (x, y) = CicAst.loc_of_floc floc in
-          let red = buf#create_tag [`FOREGROUND "red"] in
-          let (start_error_pos, end_error_pos) =
-            buf#end_iter#backward_chars (String.length last_phrase - x),
-            buf#end_iter#backward_chars (String.length last_phrase - y)
-          in
-          if x - y = 0 then (* no region to highlight, let's add an hint about
-                            where the error occured *)
-            buf#insert ~iter:end_error_pos ~tags:[red] bullet
-          else  (* highlight the region where the error occured *)
-            buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos;
-          self#echo_error (sprintf "at character %d-%d: %s" x y msg);
-          false
-      | exn ->
-          self#echo_error (sprintf "Uncaught exception: %s"
-            (Printexc.to_string exn));
-          false
+      try self#set_phrase history#next with MatitaMisc.History_failure -> ()
+
+    method wrap_exn: 'a. (unit -> 'a) -> 'a option =
+      fun f ->
+        try
+          Some (f ())
+        with exn ->
+          (match exn with (* highlight parse errors in user input *)
+          | CicTextualParser2.Parse_error (floc, msg) ->
+              let buf = self#buffer in
+              let (x, y) = CicAst.loc_of_floc floc in
+              let red = buf#create_tag [`FOREGROUND "red"] in
+              let (start_error_pos, end_error_pos) =
+                buf#end_iter#backward_chars (String.length last_phrase - x),
+                buf#end_iter#backward_chars (String.length last_phrase - y)
+              in
+              if x - y = 0 then (* no region to highlight, let's add an hint
+                                about where the error occured *)
+                buf#insert ~iter:end_error_pos ~tags:[red] bullet
+              else  (* highlight the region where the error occured *)
+                buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos;
+          | _ -> ());
+          self#echo_error (explain exn);
+          None
 
   end