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