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 type callback = string -> command_outcome
  31
  32 let default_prompt = "# "
  33 let default_phrase_sep = "."
  34 let default_callback = fun (phrase: string) -> (true, true)
  35 let bullet = "∙"
  36
  37 let message_props = [ `STYLE `ITALIC ]
  38 let error_props = [ `WEIGHT `BOLD ]
  39 let prompt_props = [ ]
  40
  41 let trailing_NL_RE = Pcre.regexp "\n\\s*$"
  42
  43 class console
  44   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
  45   ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj
  46 =
  47   let console_height = 100 in (* pixels *)
  48   object (self)
  49     inherit GText.view obj
  50
  51     val mutable _phrase_sep = phrase_sep
  52     method phrase_sep = _phrase_sep
  53     method set_phrase_sep sep = _phrase_sep <- sep
  54
  55     val mutable _prompt = prompt
  56     method prompt = _prompt
  57     method set_prompt prompt = _prompt <- prompt
  58
  59     val mutable _callback = callback
  60     method set_callback f = _callback <- f
  61
  62     val mutable _ignore_insert_text_signal = false
  63     method ignore_insert_text_signal ignore =
  64       _ignore_insert_text_signal <- ignore
  65
  66     val history =
  67       new MatitaMisc.shell_history BuildTimeConf.console_history_size
  68
  69     val mutable handle_position = 450
  70     val mutable last_phrase = ""
  71
  72     initializer
  73       let buf = self#buffer in
  74       self#set_wrap_mode `CHAR;
  75       self#hide ();
  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
  81         GdkKeysyms._Return
  82         (fun () ->
  83           buf#insert ~iter:buf#end_iter "\n";
  84           let inserted_text =
  85             MatitaMisc.strip_trailing_blanks
  86               (buf#get_text
  87                 ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
  88                 ~stop:buf#end_iter ())
  89           in
  90           self#invoke_callback inserted_text;
  91           self#echo_prompt ());
  92
  93 (*
  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)
 100         then
 101           let inserted_text =
 102             MatitaMisc.strip_trailing_blanks
 103               (buf#get_text
 104                 ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
 105                 ~stop:buf#end_iter ())
 106           in
 107           let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
 108           if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
 109             self#lock;
 110             last_phrase <- inserted_text;
 111             self#invoke_callback inserted_text;
 112             self#echo_prompt ()
 113           end));
 114 *)
 115       (match evbox with (* history key bindings *)
 116       | None -> ()
 117       | Some evbox ->
 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);
 121             ]);
 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))
 130
 131     method private set_phrase phrase =
 132       let buf = self#buffer in
 133       buf#delete
 134         ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
 135         ~stop:buf#end_iter;
 136       buf#insert ~iter:buf#end_iter phrase
 137
 138     method private invoke_callback phrase =
 139       history#add phrase;
 140       let (success, hide) = _callback phrase in
 141       if hide then self#hide ()
 142
 143     method clear () =
 144       let buf = self#buffer in
 145       buf#delete ~start:buf#start_iter ~stop:buf#end_iter
 146
 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
 153
 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;
 159       self#lock
 160
 161     method echo_message msg =
 162       self#show ();
 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]
 166         (msg ^ "\n");
 167       self#ignore_insert_text_signal false;
 168       self#lock
 169
 170     method echo_error msg =
 171       self#show ();
 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]
 175         (msg ^ "\n");
 176       self#ignore_insert_text_signal false;
 177       self#lock
 178
 179     method private get_paned_prop s =
 180       Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int }
 181         paned#as_widget
 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"
 185
 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 *)
 192       ()
 193 (*       paned#set_position self#get_max_position *)
 194     method toggle () =
 195       let pos = self#get_position in
 196       if pos > self#get_max_position - console_height then
 197         self#show ()
 198       else
 199         self#hide ()
 200
 201       (** navigation methods: history, cursor motion, ... *)
 202
 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 -> ()
 207
 208     method wrap_exn: 'a. (unit -> 'a) -> 'a option =
 209       fun f ->
 210         try
 211           Some (f ())
 212         with exn ->
 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)
 221               in
 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;
 227           | _ -> ());
 228           self#echo_error (explain exn);
 229           None
 230
 231   end
 232
 233 let console
 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 ()
 238 =
 239   let view =
 240     GText.view
 241       ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
 242       ?width ?height ?packing ?show ()
 243   in
 244   new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view
 245
 246 (* vim: set encoding=utf8: *)