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 class console
  39   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
  40   ?(callback = default_callback)
  41   obj
  42 =
  43   object (self)
  44     inherit GText.view obj
  45
  46     val mutable _phrase_sep = phrase_sep
  47     method phrase_sep = _phrase_sep
  48     method set_phrase_sep sep = _phrase_sep <- sep
  49
  50     val mutable _callback = callback
  51     method set_callback f = _callback <- f
  52
  53     val mutable _ignore_insert_text_signal = false
  54     method ignore_insert_text_signal ignore =
  55       _ignore_insert_text_signal <- ignore
  56
  57 (*
  58     (* TODO Zack: implement history.
  59        IDEA: use CTRL-P/N a la emacs.
  60        ISSUE: per-phrase or per-line history? *)
  61     val phrases_history = Array.create history_size None
  62     val mutable history_last_index = -1
  63     val mutable history_cur_index = -1
  64 *)
  65
  66     initializer
  67       let buf = self#buffer in
  68       self#set_wrap_mode `CHAR;
  69         (* create "USER_INPUT_START" mark. This mark will always point to the
  70         * beginning of user input not yet processed *)
  71       ignore (buf#create_mark ~name:"USER_INPUT_START"
  72         ~left_gravity:true buf#start_iter);
  73       ignore (buf#connect#after#insert_text (fun iter text ->
  74         if (not _ignore_insert_text_signal) &&
  75           (iter#compare buf#end_iter = 0) &&  (* insertion at end *)
  76           (Pcre.pmatch ~rex:trailing_NL_RE text)
  77         then
  78           let inserted_text =
  79             buf#get_text
  80               ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
  81               ~stop:buf#end_iter ()
  82           in
  83           let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
  84           if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
  85             self#lock;
  86             _callback inserted_text;
  87             self#echo_prompt ()
  88           end))
  89
  90       (* lock old text and bump USER_INPUT_START mark *)
  91     method private lock =
  92       let buf = self#buffer in
  93       let read_only = buf#create_tag [`EDITABLE false] in
  94       buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter;
  95       buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter
  96
  97     method echo_prompt () =
  98       let buf = self#buffer in
  99       self#ignore_insert_text_signal true;
 100       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt;
 101       self#ignore_insert_text_signal false;
 102       self#lock
 103
 104     method echo_message msg =
 105       let buf = self#buffer in
 106       self#ignore_insert_text_signal true;
 107       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props]
 108         (msg ^ "\n");
 109       self#ignore_insert_text_signal false;
 110       self#lock
 111
 112     method echo_error msg =
 113       let buf = self#buffer in
 114       self#ignore_insert_text_signal true;
 115       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
 116         (msg ^ "\n");
 117       self#ignore_insert_text_signal false;
 118       self#lock
 119   end
 120
 121 let console
 122   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
 123   ?(callback = default_callback)
 124   ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
 125   ?width ?height ?packing ?show ()
 126 =
 127   let view =
 128     GText.view
 129       ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
 130       ?width ?height ?packing ?show ()
 131   in
 132   new console ~prompt ~phrase_sep ~callback view#as_view
 133