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   object (self)
  74     inherit GText.view obj
  75
  76     val mutable _phrase_sep = phrase_sep
  77     method phrase_sep = _phrase_sep
  78     method set_phrase_sep sep = _phrase_sep <- sep
  79
  80     val mutable _prompt = prompt
  81     method prompt = _prompt
  82     method set_prompt prompt = _prompt <- prompt
  83
  84     val mutable _callback = callback
  85     method set_callback f = _callback <- f
  86
  87     val mutable _ignore_insert_text_signal = false
  88     method ignore_insert_text_signal ignore =
  89       _ignore_insert_text_signal <- ignore
  90
  91     val history = new history BuildTimeConf.console_history_size
  92
  93     val mutable handle_position = 450
  94
  95     initializer
  96       let buf = self#buffer in
  97       self#set_wrap_mode `CHAR;
  98       self#hide ();
  99         (* create "USER_INPUT_START" mark. This mark will always point to the
 100         * beginning of user input not yet processed *)
 101       ignore (buf#create_mark ~name:"USER_INPUT_START"
 102         ~left_gravity:true buf#start_iter);
 103       ignore (buf#connect#after#insert_text (fun iter text ->
 104         if (not _ignore_insert_text_signal) &&
 105           (iter#compare buf#end_iter = 0) &&  (* insertion at end *)
 106           (Pcre.pmatch ~rex:trailing_NL_RE text)
 107         then
 108           let inserted_text =
 109             buf#get_text
 110               ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
 111               ~stop:buf#end_iter ()
 112           in
 113           let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
 114           if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
 115             self#lock;
 116             self#invoke_callback inserted_text;
 117             self#echo_prompt ()
 118           end));
 119       (match evbox with (* history key bindings *)
 120       | None -> ()
 121       | Some evbox ->
 122           List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox)
 123             [ GdkKeysyms._p, (fun () -> self#previous_phrase);
 124               GdkKeysyms._n, (fun () -> self#next_phrase);
 125             ]);
 126       ignore (self#connect#after#move_cursor
 127         (* avoid cursor being placed at prompt's left *)
 128         ~callback:(fun step count ~extend ->
 129             let buf = self#buffer in
 130             let cursor_iter = buf#get_iter_at_mark `INSERT in
 131             let prompt_iter = buf#get_iter_at_mark (`NAME "USER_INPUT_START") in
 132             if prompt_iter#compare cursor_iter = 1 then (* prompt > cursor *)
 133               buf#place_cursor ~where:prompt_iter))
 134
 135     method private set_phrase phrase =
 136       let buf = self#buffer in
 137       buf#delete
 138         ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
 139         ~stop:buf#end_iter;
 140       buf#insert ~iter:buf#end_iter phrase
 141
 142     method private invoke_callback phrase =
 143       history#add (* do not push trailing phrase separator *)
 144         (String.sub phrase 0
 145           (String.length phrase - String.length _phrase_sep));
 146       if _callback phrase then
 147         self#hide ()
 148         (* else callback encountered troubles, don't hide console which
 149         probably contains error message *)
 150
 151     method clear () =
 152       let buf = self#buffer in
 153       buf#delete ~start:buf#start_iter ~stop:buf#end_iter
 154
 155       (* lock old text and bump USER_INPUT_START mark *)
 156     method private lock =
 157       let buf = self#buffer in
 158       let read_only = buf#create_tag [`EDITABLE false] in
 159       buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter;
 160       buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter
 161
 162     method echo_prompt () =
 163       let buf = self#buffer in
 164       self#ignore_insert_text_signal true;
 165       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt;
 166       self#ignore_insert_text_signal false;
 167       self#lock
 168
 169     method echo_message msg =
 170       let buf = self#buffer in
 171       self#ignore_insert_text_signal true;
 172       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props]
 173         (msg ^ "\n");
 174       self#ignore_insert_text_signal false;
 175       self#lock
 176
 177     method echo_error msg =
 178       self#show ();
 179       let buf = self#buffer in
 180       self#ignore_insert_text_signal true;
 181       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
 182         (msg ^ "\n");
 183       self#ignore_insert_text_signal false;
 184       self#lock
 185
 186     method show ?(msg = "") () =
 187       self#buffer#insert msg;
 188       paned#set_position handle_position;
 189       self#misc#grab_focus ()
 190     method hide () =
 191       self#clear ();
 192       paned#set_position max_int
 193
 194       (** navigation methods: history, cursor motion, ... *)
 195
 196     method private previous_phrase =
 197       try self#set_phrase history#previous with History_failure -> ()
 198     method private next_phrase =
 199       try self#set_phrase history#next with History_failure -> ()
 200
 201     method wrap_exn f =
 202       try
 203         f ()
 204       with exn ->
 205         self#echo_error (sprintf "Uncaught exception: %s"
 206           (Printexc.to_string exn))
 207
 208   end
 209
 210 let console
 211   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
 212   ?(callback = default_callback) ?evbox ~paned
 213   ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
 214   ?width ?height ?packing ?show ()
 215 =
 216   let view =
 217     GText.view
 218       ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
 219       ?width ?height ?packing ?show ()
 220   in
 221   new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view
 222