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