X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.ml;h=8dc43a093d3ba5f77205db126af45daf40499833;hb=eb5345bc1314ca8bf8b9ea2293dbe0aa496b2d69;hp=c1866f3f36efb6cf54121b0532ec24cbab9d9fd8;hpb=481992ea591bf53cba758a96e7d42e9cdce7e129;p=helm.git diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index c1866f3f3..8dc43a093 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -23,38 +23,216 @@ * http://helm.cs.unibo.it/ *) -let default_prompt = "## " +open Printf + +open MatitaTypes + +type callback = string -> command_outcome + +let default_prompt = "# " +let default_phrase_sep = "." +let default_callback = fun (phrase: string) -> (true, true) +let bullet = "∙" let message_props = [ `STYLE `ITALIC ] let error_props = [ `WEIGHT `BOLD ] +let prompt_props = [ ] + +let trailing_NL_RE = Pcre.regexp "\n\\s*$" -class console ?(prompt = default_prompt) obj = -(* let read_only = console#buffer#create_tag [ `EDITABLE false ] in *) +class console + ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) + ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj += + let console_height = 100 in (* pixels *) object (self) inherit GText.view obj - method read_phrase () = prompt ^ "foo" - method echo_prompt () = + val mutable _phrase_sep = phrase_sep + 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 + + val mutable _ignore_insert_text_signal = false + method ignore_insert_text_signal ignore = + _ignore_insert_text_signal <- ignore + + 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 - buf#insert ~iter:buf#end_iter ~tags:[] prompt; - self#lock + 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 = + 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 -> + 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 = let buf = self#buffer in let read_only = buf#create_tag [`EDITABLE false] in - buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter + buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter; + buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter + + method echo_prompt () = + let buf = self#buffer in + self#ignore_insert_text_signal true; + buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt; + self#ignore_insert_text_signal false; + 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] (msg ^ "\n"); + self#ignore_insert_text_signal false; 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) +let console + ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) + ?(callback = default_callback) ?evbox ~paned ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () = @@ -63,5 +241,6 @@ let console ?(prompt = default_prompt) ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () in - new console ~prompt view#as_view + new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view +(* vim: set encoding=utf8: *)