let default_phrase_sep = "."
let default_callback = fun (phrase: string) -> ()
-let history_size = 100
-
let message_props = [ `STYLE `ITALIC ]
let error_props = [ `WEIGHT `BOLD ]
let prompt_props = [ ]
method ignore_insert_text_signal ignore =
_ignore_insert_text_signal <- ignore
- val history = new history history_size
+ val history = new history BuildTimeConf.console_history_size
initializer
let buf = self#buffer in
self#invoke_callback inserted_text;
self#echo_prompt ()
end));
- (match evbox with
+ (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);
- GdkKeysyms._a, (fun () -> self#beginning_of_phrase);
- GdkKeysyms._e, (fun () -> self#end_of_phrase);
- GdkKeysyms._f, (fun () -> self#forward_char);
- GdkKeysyms._b, (fun () -> self#backward_char);
- ])
+ ]);
+ 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
try self#set_phrase history#previous with History_failure -> ()
method private next_phrase =
try self#set_phrase history#next with History_failure -> ()
- method private beginning_of_phrase =
- let buf = self#buffer in
- buf#place_cursor ~where:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
- method private end_of_phrase =
- let buf = self#buffer in
- buf#place_cursor ~where:buf#end_iter
- method private forward_char =
- let buf = self#buffer in
- buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#forward_char
- method private backward_char =
- let buf = self#buffer in
- buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#backward_char
end