X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.ml;h=8dc43a093d3ba5f77205db126af45daf40499833;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=eb77ffa5d62ac8f95bac2b34ff198cd438f8ceaf;hpb=190e42f1030ea3d459c4040bb0e8503a7c096820;p=helm.git diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index eb77ffa5d..8dc43a093 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -23,9 +23,16 @@ * http://helm.cs.unibo.it/ *) +open Printf + +open MatitaTypes + +type callback = string -> command_outcome + let default_prompt = "# " let default_phrase_sep = "." -let default_callback = fun (phrase: string) -> () +let default_callback = fun (phrase: string) -> (true, true) +let bullet = "∙" let message_props = [ `STYLE `ITALIC ] let error_props = [ `WEIGHT `BOLD ] @@ -33,38 +40,11 @@ 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 obj + ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj = + let console_height = 100 in (* pixels *) object (self) inherit GText.view obj @@ -83,31 +63,55 @@ 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 = "" initializer let buf = self#buffer in self#set_wrap_mode `CHAR; + self#hide (); (* 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); + 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 *) (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 () + MatitaMisc.strip_trailing_blanks + (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; + last_phrase <- inserted_text; self#invoke_callback inserted_text; self#echo_prompt () end)); +*) (match evbox with (* history key bindings *) | None -> () | Some evbox -> @@ -132,10 +136,13 @@ class console buf#insert ~iter:buf#end_iter phrase method private invoke_callback phrase = - history#add (* do not push trailing phrase separator *) - (String.sub phrase 0 - (String.length phrase - String.length _phrase_sep)); - _callback phrase + history#add phrase; + let (success, hide) = _callback phrase in + if hide then self#hide () + + method clear () = + let buf = self#buffer in + buf#delete ~start:buf#start_iter ~stop:buf#end_iter (* lock old text and bump USER_INPUT_START mark *) method private lock = @@ -152,6 +159,7 @@ class console self#lock method echo_message msg = + self#show (); let buf = self#buffer in self#ignore_insert_text_signal true; buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props] @@ -160,26 +168,71 @@ class console self#lock method echo_error msg = + self#show (); 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 -(* self#echo_prompt () *) + + method private get_paned_prop s = + Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int } + paned#as_widget + method private get_position = self#get_paned_prop "position" + method private get_min_position = self#get_paned_prop "min-position" + method private get_max_position = self#get_paned_prop "max-position" + + method show ?(msg = "") () = + self#buffer#insert msg; + paned#set_position (self#get_max_position - console_height); + self#misc#grab_focus () + 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 + self#show () + else + self#hide () (** 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 -> + 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 let console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) - ?(callback = default_callback) ?evbox + ?(callback = default_callback) ?evbox ~paned ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () = @@ -188,5 +241,6 @@ let console ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () in - new console ~prompt ~phrase_sep ~callback ?evbox view#as_view + new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view +(* vim: set encoding=utf8: *)