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 let default_prompt = "# "
  27 let default_phrase_sep = "."
  28 let default_callback = fun (phrase: string) -> ()
  29
  30 let history_size = 100
  31
  32 let message_props = [ `STYLE `ITALIC ]
  33 let error_props = [ `WEIGHT `BOLD ]
  34 let prompt_props = [ ]
  35
  36 let trailing_NL_RE = Pcre.regexp "\n\\s*$"
  37
  38 exception History_failure
  39
  40   (** shell like phrase history *)
  41 class history size =
  42   let size = size + 1 in
  43   let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
  44   let incr x = (x + 1) mod size in
  45   object
  46     val data = Array.create size ""
  47     val mutable hd = 0  (* insertion point *)
  48     val mutable tl = -1 (* oldest inserted item *)
  49     val mutable cur = -1  (* current item for the history *)
  50     method add s =
  51       data.(hd) <- s;
  52       if tl = -1 then tl <- hd;
  53       hd <- incr hd;
  54       if hd = tl then tl <- incr tl;
  55       cur <- hd
  56     method previous =
  57       if cur = tl then raise History_failure;
  58       cur <- decr cur;
  59       data.(cur)
  60     method next =
  61       if cur = hd then raise History_failure;
  62       cur <- incr cur;
  63       if cur = hd then "" else data.(cur)
  64   end
  65
  66 class console
  67   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
  68   ?(callback = default_callback) ?evbox obj
  69 =
  70   object (self)
  71     inherit GText.view obj
  72
  73     val mutable _phrase_sep = phrase_sep
  74     method phrase_sep = _phrase_sep
  75     method set_phrase_sep sep = _phrase_sep <- sep
  76
  77     val mutable _prompt = prompt
  78     method prompt = _prompt
  79     method set_prompt prompt = _prompt <- prompt
  80
  81     val mutable _callback = callback
  82     method set_callback f = _callback <- f
  83
  84     val mutable _ignore_insert_text_signal = false
  85     method ignore_insert_text_signal ignore =
  86       _ignore_insert_text_signal <- ignore
  87
  88     val history = new history history_size
  89
  90     initializer
  91       let buf = self#buffer in
  92       self#set_wrap_mode `CHAR;
  93         (* create "USER_INPUT_START" mark. This mark will always point to the
  94         * beginning of user input not yet processed *)
  95       ignore (buf#create_mark ~name:"USER_INPUT_START"
  96         ~left_gravity:true buf#start_iter);
  97       ignore (buf#connect#after#insert_text (fun iter text ->
  98         if (not _ignore_insert_text_signal) &&
  99           (iter#compare buf#end_iter = 0) &&  (* insertion at end *)
 100           (Pcre.pmatch ~rex:trailing_NL_RE text)
 101         then
 102           let inserted_text =
 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             self#invoke_callback inserted_text;
 111             self#echo_prompt ()
 112           end));
 113       (match evbox with
 114       | None -> ()
 115       | Some evbox ->
 116           List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox)
 117             [ GdkKeysyms._p, (fun () -> self#previous_phrase);
 118               GdkKeysyms._n, (fun () -> self#next_phrase);
 119               GdkKeysyms._a, (fun () -> self#beginning_of_phrase);
 120               GdkKeysyms._e, (fun () -> self#end_of_phrase);
 121               GdkKeysyms._f, (fun () -> self#forward_char);
 122               GdkKeysyms._b, (fun () -> self#backward_char);
 123             ])
 124
 125     method private set_phrase phrase =
 126       let buf = self#buffer in
 127       buf#delete
 128         ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
 129         ~stop:buf#end_iter;
 130       buf#insert ~iter:buf#end_iter phrase
 131
 132     method private invoke_callback phrase =
 133       history#add (* do not push trailing phrase separator *)
 134         (String.sub phrase 0
 135           (String.length phrase - String.length _phrase_sep));
 136       _callback phrase
 137
 138       (* lock old text and bump USER_INPUT_START mark *)
 139     method private lock =
 140       let buf = self#buffer in
 141       let read_only = buf#create_tag [`EDITABLE false] in
 142       buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter;
 143       buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter
 144
 145     method echo_prompt () =
 146       let buf = self#buffer in
 147       self#ignore_insert_text_signal true;
 148       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt;
 149       self#ignore_insert_text_signal false;
 150       self#lock
 151
 152     method echo_message msg =
 153       let buf = self#buffer in
 154       self#ignore_insert_text_signal true;
 155       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props]
 156         (msg ^ "\n");
 157       self#ignore_insert_text_signal false;
 158       self#lock
 159
 160     method echo_error msg =
 161       let buf = self#buffer in
 162       self#ignore_insert_text_signal true;
 163       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
 164         (msg ^ "\n");
 165       self#ignore_insert_text_signal false;
 166       self#lock
 167
 168       (** navigation methods: history, cursor motion, ... *)
 169
 170     method private previous_phrase =
 171       try self#set_phrase history#previous with History_failure -> ()
 172     method private next_phrase =
 173       try self#set_phrase history#next with History_failure -> ()
 174     method private beginning_of_phrase =
 175       let buf = self#buffer in
 176       buf#place_cursor ~where:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
 177     method private end_of_phrase =
 178       let buf = self#buffer in
 179       buf#place_cursor ~where:buf#end_iter
 180     method private forward_char =
 181       let buf = self#buffer in
 182       buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#forward_char
 183     method private backward_char =
 184       let buf = self#buffer in
 185       buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#backward_char
 186
 187   end
 188
 189 let console
 190   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
 191   ?(callback = default_callback) ?evbox
 192   ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
 193   ?width ?height ?packing ?show ()
 194 =
 195   let view =
 196     GText.view
 197       ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
 198       ?width ?height ?packing ?show ()
 199   in
 200   new console ~prompt ~phrase_sep ~callback ?evbox view#as_view
 201