(* Copyright (C) 2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) open Printf open MatitaTypes type callback = string -> command_outcome let default_prompt = "# " let default_phrase_sep = "." let default_callback = fun (phrase: string) -> (true, true) let bullet = "∙" let message_props = [ `STYLE `ITALIC ] let error_props = [ `WEIGHT `BOLD ] let prompt_props = [ ] let trailing_NL_RE = Pcre.regexp "\n\\s*$" class console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj = let console_height = 100 in (* pixels *) object (self) inherit GText.view obj val mutable _phrase_sep = phrase_sep method phrase_sep = _phrase_sep method set_phrase_sep sep = _phrase_sep <- sep val mutable _prompt = prompt method prompt = _prompt method set_prompt prompt = _prompt <- prompt val mutable _callback = callback method set_callback f = _callback <- f val mutable _ignore_insert_text_signal = false method ignore_insert_text_signal ignore = _ignore_insert_text_signal <- ignore val history = new MatitaMisc.shell_history BuildTimeConf.console_history_size val mutable handle_position = 450 val mutable last_phrase = "" initializer let buf = self#buffer in self#set_wrap_mode `CHAR; self#hide (); (* create "USER_INPUT_START" mark. This mark will always point to the * beginning of user input not yet processed *) ignore (buf#create_mark ~name:"USER_INPUT_START" ~left_gravity:true buf#start_iter); MatitaGtkMisc.connect_key self#event ~modifiers:[`CONTROL] ~stop:true GdkKeysyms._Return (fun () -> buf#insert ~iter:buf#end_iter "\n"; let inserted_text = MatitaMisc.strip_trailing_blanks (buf#get_text ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) ~stop:buf#end_iter ()) in self#invoke_callback inserted_text; self#echo_prompt ()); (* (* callback handling based on phrase terminator (e.g. ";;" at the end of * the row: each time a character is inserted *) ignore (buf#connect#after#insert_text (fun iter text -> if (not _ignore_insert_text_signal) && (iter#compare buf#end_iter = 0) && (* insertion at end *) (Pcre.pmatch ~rex:trailing_NL_RE text) then let inserted_text = MatitaMisc.strip_trailing_blanks (buf#get_text ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) ~stop:buf#end_iter ()) in let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *) self#lock; last_phrase <- inserted_text; self#invoke_callback inserted_text; self#echo_prompt () end)); *) (match evbox with (* history key bindings *) | None -> () | Some evbox -> List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox) [ GdkKeysyms._p, (fun () -> self#previous_phrase); GdkKeysyms._n, (fun () -> self#next_phrase); ]); ignore (self#connect#after#move_cursor (* avoid cursor being placed at prompt's left *) ~callback:(fun step count ~extend -> let buf = self#buffer in let cursor_iter = buf#get_iter_at_mark `INSERT in let prompt_iter = buf#get_iter_at_mark (`NAME "USER_INPUT_START") in if prompt_iter#compare cursor_iter = 1 then (* prompt > cursor *) buf#place_cursor ~where:prompt_iter)) method private set_phrase phrase = let buf = self#buffer in buf#delete ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) ~stop:buf#end_iter; buf#insert ~iter:buf#end_iter phrase method private invoke_callback phrase = history#add phrase; let (success, hide) = _callback phrase in if hide then self#hide () method clear () = let buf = self#buffer in buf#delete ~start:buf#start_iter ~stop:buf#end_iter (* lock old text and bump USER_INPUT_START mark *) method private lock = let buf = self#buffer in let read_only = buf#create_tag [`EDITABLE false] in buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter; buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter method echo_prompt () = let buf = self#buffer in self#ignore_insert_text_signal true; buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt; self#ignore_insert_text_signal false; self#lock method echo_message msg = self#show (); let buf = self#buffer in self#ignore_insert_text_signal true; buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props] (msg ^ "\n"); self#ignore_insert_text_signal false; self#lock method echo_error msg = self#show (); let buf = self#buffer in self#ignore_insert_text_signal true; buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props] (msg ^ "\n"); self#ignore_insert_text_signal false; self#lock method private get_paned_prop s = Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int } paned#as_widget method private get_position = self#get_paned_prop "position" method private get_min_position = self#get_paned_prop "min-position" method private get_max_position = self#get_paned_prop "max-position" method show ?(msg = "") () = self#buffer#insert msg; paned#set_position (self#get_max_position - console_height); self#misc#grab_focus () method hide () = (* ZACK still not sure about the gui, for the moment just * keep the console persistent *) () (* paned#set_position self#get_max_position *) method toggle () = let pos = self#get_position in if pos > self#get_max_position - console_height then self#show () else self#hide () (** navigation methods: history, cursor motion, ... *) method private previous_phrase = try self#set_phrase history#previous with MatitaMisc.History_failure -> () method private next_phrase = try self#set_phrase history#next with MatitaMisc.History_failure -> () method wrap_exn: 'a. (unit -> 'a) -> 'a option = fun f -> try Some (f ()) with exn -> (match exn with (* highlight parse errors in user input *) | CicTextualParser2.Parse_error (floc, msg) -> let buf = self#buffer in let (x, y) = CicAst.loc_of_floc floc in let red = buf#create_tag [`FOREGROUND "red"] in let (start_error_pos, end_error_pos) = buf#end_iter#backward_chars (String.length last_phrase - x), buf#end_iter#backward_chars (String.length last_phrase - y) in if x - y = 0 then (* no region to highlight, let's add an hint about where the error occured *) buf#insert ~iter:end_error_pos ~tags:[red] bullet else (* highlight the region where the error occured *) buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos; | _ -> ()); self#echo_error (explain exn); None end let console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) ?(callback = default_callback) ?evbox ~paned ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () = let view = GText.view ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () in new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view (* vim: set encoding=utf8: *)