X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.ml;h=8dc43a093d3ba5f77205db126af45daf40499833;hb=2026624f827b29c35d54aa67b301250123ea7311;hp=9c3c5a9b5aa7fb702ffa64f0d1e2e9695a91f7cf;hpb=4cf419a2e770f4971be7b03b1d73e585d973dc1b;p=helm.git diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 9c3c5a9b5..8dc43a093 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -23,11 +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 history_size = 100 +let default_callback = fun (phrase: string) -> (true, true) +let bullet = "∙" let message_props = [ `STYLE `ITALIC ] let error_props = [ `WEIGHT `BOLD ] @@ -37,9 +42,9 @@ let trailing_NL_RE = Pcre.regexp "\n\\s*$" class console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) - ?(callback = default_callback) - obj + ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj = + let console_height = 100 in (* pixels *) object (self) inherit GText.view obj @@ -47,6 +52,10 @@ class console method phrase_sep = _phrase_sep method set_phrase_sep sep = _phrase_sep <- sep + val mutable _prompt = prompt + method prompt = _prompt + method set_prompt prompt = _prompt <- prompt + val mutable _callback = callback method set_callback f = _callback <- f @@ -54,38 +63,86 @@ class console method ignore_insert_text_signal ignore = _ignore_insert_text_signal <- ignore -(* - (* TODO Zack: implement history. - IDEA: use CTRL-P/N a la emacs. - ISSUE: per-phrase or per-line history? *) - val phrases_history = Array.create history_size None - val mutable history_last_index = -1 - val mutable history_cur_index = -1 -*) + 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; - _callback inserted_text; + last_phrase <- inserted_text; + self#invoke_callback inserted_text; self#echo_prompt () - end)) + end)); +*) + (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); + ]); + 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 + buf#delete + ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) + ~stop:buf#end_iter; + buf#insert ~iter:buf#end_iter phrase + + method private invoke_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 = @@ -102,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] @@ -110,17 +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 + + 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 MatitaMisc.History_failure -> () + method private next_phrase = + 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) + ?(callback = default_callback) ?evbox ~paned ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () = @@ -129,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 view#as_view + new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view +(* vim: set encoding=utf8: *)