X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.ml;h=8dc43a093d3ba5f77205db126af45daf40499833;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=222055e6539a59b8b9ecfed8bf3434d746bcb936;hpb=e35ec00b1be70e4b064b74a49735b37b5e719e5b;p=helm.git diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 222055e65..8dc43a093 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -27,10 +27,12 @@ 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 ] let error_props = [ `WEIGHT `BOLD ] @@ -38,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 @@ -89,9 +63,11 @@ 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 @@ -101,22 +77,41 @@ 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 *) (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 -> @@ -141,15 +136,9 @@ 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)); - if _callback phrase then begin - self#hide (); - self#clear () - (* else callback encountered troubles, don't hide console which - probably contains error message *) - end + history#add phrase; + let (success, hide) = _callback phrase in + if hide then self#hide () method clear () = let buf = self#buffer in @@ -170,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] @@ -197,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 @@ -209,22 +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 - | 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 @@ -241,3 +243,4 @@ let console in new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view +(* vim: set encoding=utf8: *)