1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 type callback = string -> command_outcome
32 let default_prompt = "# "
33 let default_phrase_sep = "."
34 let default_callback = fun (phrase: string) -> (true, true)
37 let message_props = [ `STYLE `ITALIC ]
38 let error_props = [ `WEIGHT `BOLD ]
39 let prompt_props = [ ]
41 let trailing_NL_RE = Pcre.regexp "\n\\s*$"
44 ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
45 ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj
47 let console_height = 100 in (* pixels *)
49 inherit GText.view obj
51 val mutable _phrase_sep = phrase_sep
52 method phrase_sep = _phrase_sep
53 method set_phrase_sep sep = _phrase_sep <- sep
55 val mutable _prompt = prompt
56 method prompt = _prompt
57 method set_prompt prompt = _prompt <- prompt
59 val mutable _callback = callback
60 method set_callback f = _callback <- f
62 val mutable _ignore_insert_text_signal = false
63 method ignore_insert_text_signal ignore =
64 _ignore_insert_text_signal <- ignore
67 new MatitaMisc.shell_history BuildTimeConf.console_history_size
69 val mutable handle_position = 450
70 val mutable last_phrase = ""
73 let buf = self#buffer in
74 self#set_wrap_mode `CHAR;
76 (* create "USER_INPUT_START" mark. This mark will always point to the
77 * beginning of user input not yet processed *)
78 ignore (buf#create_mark ~name:"USER_INPUT_START"
79 ~left_gravity:true buf#start_iter);
80 MatitaGtkMisc.connect_key self#event ~modifiers:[`CONTROL] ~stop:true
83 buf#insert ~iter:buf#end_iter "\n";
85 MatitaMisc.strip_trailing_blanks
87 ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
88 ~stop:buf#end_iter ())
90 self#invoke_callback inserted_text;
94 (* callback handling based on phrase terminator (e.g. ";;" at the end of
95 * the row: each time a character is inserted *)
96 ignore (buf#connect#after#insert_text (fun iter text ->
97 if (not _ignore_insert_text_signal) &&
98 (iter#compare buf#end_iter = 0) && (* insertion at end *)
99 (Pcre.pmatch ~rex:trailing_NL_RE text)
102 MatitaMisc.strip_trailing_blanks
104 ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
105 ~stop:buf#end_iter ())
107 let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
108 if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
110 last_phrase <- inserted_text;
111 self#invoke_callback inserted_text;
115 (match evbox with (* history key bindings *)
118 List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox)
119 [ GdkKeysyms._p, (fun () -> self#previous_phrase);
120 GdkKeysyms._n, (fun () -> self#next_phrase);
122 ignore (self#connect#after#move_cursor
123 (* avoid cursor being placed at prompt's left *)
124 ~callback:(fun step count ~extend ->
125 let buf = self#buffer in
126 let cursor_iter = buf#get_iter_at_mark `INSERT in
127 let prompt_iter = buf#get_iter_at_mark (`NAME "USER_INPUT_START") in
128 if prompt_iter#compare cursor_iter = 1 then (* prompt > cursor *)
129 buf#place_cursor ~where:prompt_iter))
131 method private set_phrase phrase =
132 let buf = self#buffer in
134 ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
136 buf#insert ~iter:buf#end_iter phrase
138 method private invoke_callback phrase =
140 let (success, hide) = _callback phrase in
141 if hide then self#hide ()
144 let buf = self#buffer in
145 buf#delete ~start:buf#start_iter ~stop:buf#end_iter
147 (* lock old text and bump USER_INPUT_START mark *)
148 method private lock =
149 let buf = self#buffer in
150 let read_only = buf#create_tag [`EDITABLE false] in
151 buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter;
152 buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter
154 method echo_prompt () =
155 let buf = self#buffer in
156 self#ignore_insert_text_signal true;
157 buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt;
158 self#ignore_insert_text_signal false;
161 method echo_message msg =
163 let buf = self#buffer in
164 self#ignore_insert_text_signal true;
165 buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props]
167 self#ignore_insert_text_signal false;
170 method echo_error msg =
172 let buf = self#buffer in
173 self#ignore_insert_text_signal true;
174 buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
176 self#ignore_insert_text_signal false;
179 method private get_paned_prop s =
180 Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int }
182 method private get_position = self#get_paned_prop "position"
183 method private get_min_position = self#get_paned_prop "min-position"
184 method private get_max_position = self#get_paned_prop "max-position"
186 method show ?(msg = "") () =
187 self#buffer#insert msg;
188 paned#set_position (self#get_max_position - console_height);
189 self#misc#grab_focus ()
190 method hide () = (* ZACK still not sure about the gui, for the moment just
191 * keep the console persistent *)
193 (* paned#set_position self#get_max_position *)
195 let pos = self#get_position in
196 if pos > self#get_max_position - console_height then
201 (** navigation methods: history, cursor motion, ... *)
203 method private previous_phrase =
204 try self#set_phrase history#previous with MatitaMisc.History_failure -> ()
205 method private next_phrase =
206 try self#set_phrase history#next with MatitaMisc.History_failure -> ()
208 method wrap_exn: 'a. (unit -> 'a) -> 'a option =
213 (match exn with (* highlight parse errors in user input *)
214 | CicTextualParser2.Parse_error (floc, msg) ->
215 let buf = self#buffer in
216 let (x, y) = CicAst.loc_of_floc floc in
217 let red = buf#create_tag [`FOREGROUND "red"] in
218 let (start_error_pos, end_error_pos) =
219 buf#end_iter#backward_chars (String.length last_phrase - x),
220 buf#end_iter#backward_chars (String.length last_phrase - y)
222 if x - y = 0 then (* no region to highlight, let's add an hint
223 about where the error occured *)
224 buf#insert ~iter:end_error_pos ~tags:[red] bullet
225 else (* highlight the region where the error occured *)
226 buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos;
228 self#echo_error (explain exn);
234 ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
235 ?(callback = default_callback) ?evbox ~paned
236 ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
237 ?width ?height ?packing ?show ()
241 ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
242 ?width ?height ?packing ?show ()
244 new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view
246 (* vim: set encoding=utf8: *)