]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/matitaConsole.ml
snapshot
[helm.git] / helm / matita / matitaConsole.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 open Printf
27
28 open MatitaTypes
29
30 (* let default_prompt = "# " *)
31 let default_prompt = ""
32 let default_phrase_sep = "."
33 let default_callback = fun (phrase: string) -> true
34
35 let message_props = [ `STYLE `ITALIC ]
36 let error_props = [ `WEIGHT `BOLD ]
37 let prompt_props = [ ]
38
39 let trailing_NL_RE = Pcre.regexp "\n\\s*$"
40
41 exception History_failure
42
43   (** shell like phrase history *)
44 class history size =
45   let size = size + 1 in
46   let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
47   let incr x = (x + 1) mod size in
48   object
49     val data = Array.create size ""
50     val mutable hd = 0  (* insertion point *)
51     val mutable tl = -1 (* oldest inserted item *)
52     val mutable cur = -1  (* current item for the history *)
53     method add s =
54       data.(hd) <- s;
55       if tl = -1 then tl <- hd;
56       hd <- incr hd;
57       if hd = tl then tl <- incr tl;
58       cur <- hd
59     method previous =
60       if cur = tl then raise History_failure;
61       cur <- decr cur;
62       data.(cur)
63     method next =
64       if cur = hd then raise History_failure;
65       cur <- incr cur;
66       if cur = hd then "" else data.(cur)
67   end
68
69 class console
70   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
71   ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj
72 =
73   let console_height = 100 in (* pixels *)
74   object (self)
75     inherit GText.view obj
76
77     val mutable _phrase_sep = phrase_sep
78     method phrase_sep = _phrase_sep
79     method set_phrase_sep sep = _phrase_sep <- sep
80
81     val mutable _prompt = prompt
82     method prompt = _prompt
83     method set_prompt prompt = _prompt <- prompt
84
85     val mutable _callback = callback
86     method set_callback f = _callback <- f
87
88     val mutable _ignore_insert_text_signal = false
89     method ignore_insert_text_signal ignore =
90       _ignore_insert_text_signal <- ignore
91
92     val history = new history BuildTimeConf.console_history_size
93
94     val mutable handle_position = 450
95
96     initializer
97       let buf = self#buffer in
98       self#set_wrap_mode `CHAR;
99       self#hide ();
100         (* create "USER_INPUT_START" mark. This mark will always point to the
101         * beginning of user input not yet processed *)
102       ignore (buf#create_mark ~name:"USER_INPUT_START"
103         ~left_gravity:true buf#start_iter);
104       ignore (buf#connect#after#insert_text (fun iter text ->
105         if (not _ignore_insert_text_signal) &&
106           (iter#compare buf#end_iter = 0) &&  (* insertion at end *)
107           (Pcre.pmatch ~rex:trailing_NL_RE text)
108         then
109           let inserted_text =
110             buf#get_text
111               ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
112               ~stop:buf#end_iter ()
113           in
114           let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
115           if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
116             self#lock;
117             self#invoke_callback inserted_text;
118             self#echo_prompt ()
119           end));
120       (match evbox with (* history key bindings *)
121       | None -> ()
122       | Some evbox ->
123           List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox)
124             [ GdkKeysyms._p, (fun () -> self#previous_phrase);
125               GdkKeysyms._n, (fun () -> self#next_phrase);
126             ]);
127       ignore (self#connect#after#move_cursor
128         (* avoid cursor being placed at prompt's left *)
129         ~callback:(fun step count ~extend ->
130             let buf = self#buffer in
131             let cursor_iter = buf#get_iter_at_mark `INSERT in
132             let prompt_iter = buf#get_iter_at_mark (`NAME "USER_INPUT_START") in
133             if prompt_iter#compare cursor_iter = 1 then (* prompt > cursor *)
134               buf#place_cursor ~where:prompt_iter))
135
136     method private set_phrase phrase =
137       let buf = self#buffer in
138       buf#delete
139         ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
140         ~stop:buf#end_iter;
141       buf#insert ~iter:buf#end_iter phrase
142
143     method private invoke_callback phrase =
144       history#add (* do not push trailing phrase separator *)
145         (String.sub phrase 0
146           (String.length phrase - String.length _phrase_sep));
147       if _callback phrase then begin
148         self#hide ();
149         self#clear ()
150         (* else callback encountered troubles, don't hide console which
151         probably contains error message *)
152       end
153
154     method clear () =
155       let buf = self#buffer in
156       buf#delete ~start:buf#start_iter ~stop:buf#end_iter
157
158       (* lock old text and bump USER_INPUT_START mark *)
159     method private lock =
160       let buf = self#buffer in
161       let read_only = buf#create_tag [`EDITABLE false] in
162       buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter;
163       buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter
164
165     method echo_prompt () =
166       let buf = self#buffer in
167       self#ignore_insert_text_signal true;
168       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt;
169       self#ignore_insert_text_signal false;
170       self#lock
171
172     method echo_message msg =
173       let buf = self#buffer in
174       self#ignore_insert_text_signal true;
175       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props]
176         (msg ^ "\n");
177       self#ignore_insert_text_signal false;
178       self#lock
179
180     method echo_error msg =
181       self#show ();
182       let buf = self#buffer in
183       self#ignore_insert_text_signal true;
184       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
185         (msg ^ "\n");
186       self#ignore_insert_text_signal false;
187       self#lock
188
189     method private get_paned_prop s =
190       Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int }
191         paned#as_widget
192     method private get_position = self#get_paned_prop "position"
193     method private get_min_position = self#get_paned_prop "min-position"
194     method private get_max_position = self#get_paned_prop "max-position"
195
196     method show ?(msg = "") () =
197       self#buffer#insert msg;
198       paned#set_position (self#get_max_position - console_height);
199       self#misc#grab_focus ()
200     method hide () =
201       paned#set_position self#get_max_position
202     method toggle () =
203       let pos = self#get_position in
204       if pos > self#get_max_position - console_height then
205         self#show ()
206       else
207         self#hide ()
208
209       (** navigation methods: history, cursor motion, ... *)
210
211     method private previous_phrase =
212       try self#set_phrase history#previous with History_failure -> ()
213     method private next_phrase =
214       try self#set_phrase history#next with History_failure -> ()
215
216     method wrap_exn (f: unit -> unit) =
217       try
218         f ();
219         true
220       with
221       | StatefulProofEngine.Tactic_failure exn ->
222           self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn));
223           false
224       | exn ->
225           self#echo_error (sprintf "Uncaught exception: %s"
226             (Printexc.to_string exn));
227           false
228
229   end
230
231 let console
232   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
233   ?(callback = default_callback) ?evbox ~paned
234   ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
235   ?width ?height ?packing ?show ()
236 =
237   let view =
238     GText.view
239       ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
240       ?width ?height ?packing ?show ()
241   in
242   new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view
243