matitaGui.cmi
matitaGui.cmx: matitaConsole.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmx \
matitaGui.cmi
+matitaInterpreter.cmo: matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi
+matitaInterpreter.cmx: matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi
matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \
- matitaGui.cmi matitaProof.cmi matitaTypes.cmo
+ matitaGui.cmi matitaInterpreter.cmi matitaProof.cmi matitaTypes.cmo
matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \
- matitaGui.cmx matitaProof.cmx matitaTypes.cmx
+ matitaGui.cmx matitaInterpreter.cmx matitaProof.cmx matitaTypes.cmx
matitaProof.cmo: matitaTypes.cmo matitaProof.cmi
matitaProof.cmx: matitaTypes.cmx matitaProof.cmi
matitaTypes.cmo: buildTimeConf.cmo
matitaDisambiguator.cmi: matitaTypes.cmo
matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmo
matitaGui.cmi: matitaGeneratedGui.cmi
+matitaInterpreter.cmi: matitaTypes.cmo
matitaProof.cmi: matitaTypes.cmo
matitaConsole.cmo \
matitaGui.cmo \
matitaProof.cmo \
- matitaDisambiguator.cmo
+ matitaDisambiguator.cmo \
+ matitaInterpreter.cmo
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
all: matita
FINDLIB_REQUIRES="\
lablgtk2.glade \
+pcre \
helm-cic_omdoc \
helm-cic_transformations \
helm-registry \
~chooseUris:(interactive_user_uri_choice ~gui)
~chooseInterp:(interactive_interp_choice ~gui)
()
+let new_proof proof =
+ (* TODO Zack: high level function which create a new proof object and register
+ * to it the widgets which must be refreshed upon status changes *)
+(* proof#status#attach ... *)
+ proof#status#notify ();
+ set_proof proof
+let interpreter =
+ new MatitaInterpreter.interpreter
+ ~disambiguator ~console:gui#console ~get_proof ~new_proof ()
(** quit program, possibly asking for confirmation *)
let quit () = GMain.Main.quit ()
let _ =
gui#setQuitCallback quit;
+ gui#setPhraseCallback interpreter#evalPhrase;
gui#main#debugMenu#misc#hide ();
ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
if has_proof () &&
disambiguator#disambiguateTerm (Stream.of_string input)
in
let proof = MatitaProof.proof ~typ:term ~metasenv () in
-(* proof#status#attach ... FINQUI *)
- proof#status#notify ();
- set_proof proof;
+ new_proof proof;
debug_print ("new proof, goal is: " ^ CicPp.ppterm term)))
(** <DEBUGGING> *)
* http://helm.cs.unibo.it/
*)
-let default_prompt = "## "
+let default_prompt = "# "
+let default_phrase_sep = "."
+let default_callback = fun (phrase: string) -> ()
+
+let history_size = 100
let message_props = [ `STYLE `ITALIC ]
let error_props = [ `WEIGHT `BOLD ]
+let prompt_props = [ ]
-class console ?(prompt = default_prompt) obj =
-(* let read_only = console#buffer#create_tag [ `EDITABLE false ] in *)
+class console
+ ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
+ ?(callback = default_callback)
+ obj
+=
+ let ui_mark = `NAME "USER_INPUT_START" in
object (self)
inherit GText.view obj
- method read_phrase () = prompt ^ "foo"
- method echo_prompt () =
+ val mutable _phrase_sep = phrase_sep
+ method phrase_sep = _phrase_sep
+ method set_phrase_sep sep = _phrase_sep <- sep
+
+ val mutable _callback = callback
+ method set_callback f = _callback <- f
+
+(*
+ (* TODO Zack: implement history.
+ IDEA: use CTRL-P/N a la emacs.
+ ISSUE: per-phrase or per-line history? *)
+ val phrases_history = Array.create history_size None
+ val mutable history_last_index = -1
+ val mutable history_cur_index = -1
+*)
+
+ initializer
let buf = self#buffer in
- buf#insert ~iter:buf#end_iter ~tags:[] prompt;
- self#lock
+ (* 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);
+ ignore (self#event#connect#key_press (fun key -> (* handle return ev. *)
+ if GdkEvent.Key.keyval key = GdkKeysyms._Return then begin
+ let insert_point = buf#get_iter_at_mark `INSERT in
+ if insert_point#compare buf#end_iter = 0 then (* insert pt. at end *)
+ let inserted_text =
+ buf#get_text ~start:(buf#get_iter_at_mark ui_mark)
+ ~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;
+ _callback inserted_text
+ end
+ end;
+ false (* continue event processing *)))
+
+ (* 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
+ let stop = buf#end_iter in
+ buf#apply_tag read_only ~start:buf#start_iter ~stop;
+ buf#move_mark ui_mark stop
+
+ method echo_prompt () =
+ let buf = self#buffer in
+ buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt;
+ self#lock
+
method echo_message msg =
let buf = self#buffer in
buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props]
(msg ^ "\n");
self#lock
+
method echo_error msg =
let buf = self#buffer in
buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
self#lock
end
-let console ?(prompt = default_prompt)
+let console
+ ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
+ ?(callback = default_callback)
?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
?width ?height ?packing ?show ()
=
?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
?width ?height ?packing ?show ()
in
- new console ~prompt view#as_view
+ new console ~prompt ~phrase_sep ~callback view#as_view
* http://helm.cs.unibo.it/
*)
-class console: ?prompt:string -> Gtk.text_view Gtk.obj ->
+class console:
+ ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) ->
+ Gtk.text_view Gtk.obj ->
object
inherit GText.view
- method read_phrase : unit -> string
+ method echo_prompt : unit -> unit
+ method echo_message : string -> unit
+ method echo_error : string -> unit
- method echo_prompt : unit -> unit
- method echo_message : string -> unit
- method echo_error : string -> unit
+ method phrase_sep : string
+ method set_phrase_sep : string -> unit
+
+ (** override previous callback definition *)
+ method set_callback : (string -> unit) -> unit
end
+ (** @param prompt user prompt (default "# ")
+ * @param phrase_sep phrase separator (default ".")
+ * @param callback callback invoked upon reading of a phrase. Callback
+ * may be invoked more than once if multiple phrases have been inserted before
+ * hitting return (default: do nothing) *)
val console :
?prompt:string ->
+ ?phrase_sep:string ->
+ ?callback:(string -> unit) ->
+
?buffer:GText.buffer ->
?editable:bool ->
?cursor_visible:bool ->
method env = _env
method setEnv e = _env <- e
- method disambiguateTermAst ?(context = []) ?(metasenv = []) ?(env = _env)
- termAst
- =
+ method disambiguateTermAst ?(context = []) ?(metasenv = []) ?env termAst =
+ let (save_state, env) =
+ match env with
+ | Some env -> (false, env)
+ | None -> (true, _env)
+ in
match disambiguate_term mqiconn context metasenv termAst ~aliases:env with
- | [ x ] -> x
+ | [ (env, metasenv, term) as x ] ->
+ if save_state then self#setEnv env;
+ x
| _ -> assert false
method disambiguateTerm ?context ?metasenv ?env stream =
* http://helm.cs.unibo.it/
*)
-class parserr: unit ->
- object
- inherit MatitaTypes.parserr
- end
+class parserr: unit -> MatitaTypes.parserr
class disambiguator:
parserr:MatitaTypes.parserr -> (** parser *)
chooseUris:MatitaTypes.choose_uris_callback ->
chooseInterp:MatitaTypes.choose_interp_callback ->
unit ->
- object
- inherit MatitaTypes.disambiguator
- end
+ MatitaTypes.disambiguator
[ toolbar#toolBarEventBox; proof#proofWinEventBox ]
in
let console = MatitaConsole.console ~packing:main#scrolledConsole#add () in
- let _ =
- console#echo_message "message";
- console#echo_error "error";
- console#echo_prompt ()
- in
object (self)
initializer
(* glade's check widgets *)
List.iter (fun w -> w#misc#set_sensitive false)
[ main#saveMenuItem; main#saveAsMenuItem ];
main#helpMenu#set_right_justified true;
- (* uri choice *)
- ()
+ (* console *)
+ console#echo_message "message";
+ console#echo_error "error";
+ console#echo_prompt ();
+ console#misc#grab_focus ()
- method toolbar = toolbar
- method main = main
method about = about
+ method console = console
method fileSel = fileSel
+ method main = main
method proof = proof
+ method toolbar = toolbar
method newUriDialog () =
let dialog = new uriChoiceDialog ~file () in
ignore (main#quitMenuItem#connect#activate callback);
self#addKeyBinding GdkKeysyms._q callback
+ method setPhraseCallback = console#set_callback
+
end
string ->
object
- method setQuitCallback : (unit -> unit) -> unit
+ method setQuitCallback : (unit -> unit) -> unit
+ method setPhraseCallback : (string -> unit) -> unit
- (** {2 Access to low-level GTK widgets} *)
+ (** {2 Access to lower-level GTK widgets} *)
method about : MatitaGeneratedGui.aboutWin
method fileSel : MatitaGeneratedGui.fileSelectionWin
method proof : MatitaGeneratedGui.proofWin
method toolbar : MatitaGeneratedGui.toolBarWin
+ (** {2 Access to GUI useful components} *)
+
+ method console: MatitaConsole.console
+
(** {2 Dialogs instantiation}
* methods below create a new window on each invocation. You should
* remember to destroy windows after use *)
--- /dev/null
+(* 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/
+ *)
+
+type state_tag = [ `Command | `Proof ]
+
+class type interpreterState =
+ object
+ (** eval a toplevel phrase in the current state and return the new state
+ *)
+ method evalPhrase: string -> state_tag
+ end
+
+class commandState
+ ~(disambiguator: MatitaTypes.disambiguator)
+ ~(console: MatitaConsole.console)
+ ~new_proof ()
+=
+ object
+ method evalPhrase s: state_tag =
+ let command = CicTextualParser2.parse_command (Stream.of_string s) in
+ match command with
+ | CommandAst.Theorem (_, _, Some name, ast, None) ->
+ let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
+ let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
+ let proof = MatitaProof.proof ~typ:expr ~metasenv () in
+ new_proof proof;
+ `Proof
+ | _ ->
+ MatitaTypes.not_implemented (* TODO Zack *)
+ "MatitaInterpreter.commandState#evalPhrase: commands other than full theorem ones";
+ `Proof
+ end
+
+class proofState
+ ~(disambiguator: MatitaTypes.disambiguator)
+ ~(console: MatitaConsole.console)
+ ~get_proof ()
+=
+ object
+ method evalPhrase (s: string): state_tag =
+ (* TODO Zack *)
+ MatitaTypes.not_implemented "MatitaInterpreter.proofState#evalPhrase";
+ `Command
+ end
+
+class interpreter
+ ~(disambiguator: MatitaTypes.disambiguator)
+ ~(console: MatitaConsole.console)
+ ~(get_proof: unit -> MatitaTypes.proof)
+ ~(new_proof: MatitaTypes.proof -> unit)
+ ()
+=
+ let commandState =
+ lazy (new commandState ~disambiguator ~console ~new_proof ())
+ in
+ let proofState =
+ lazy (new proofState ~disambiguator ~console ~get_proof ())
+ in
+ object
+ val mutable state = Lazy.force commandState
+
+ method evalPhrase s =
+ match state#evalPhrase s with
+ | `Command -> state <- Lazy.force commandState
+ | `Proof -> state <- Lazy.force proofState
+ end
+
--- /dev/null
+(* 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/
+ *)
+
+class interpreter:
+ disambiguator:MatitaTypes.disambiguator ->
+ console:MatitaConsole.console ->
+ get_proof:(unit -> MatitaTypes.proof) ->
+ new_proof:(MatitaTypes.proof -> unit) ->
+ unit ->
+ MatitaTypes.interpreter
+
exception No_proof (** no current proof is available *)
let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
-let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def"
+let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
class type observer =
(* "observer" pattern *)
(* TODO Zack: as long as matita doesn't support MDI inteface,
* disambiguateTerm will return a single term *)
- (** @param env defaults to self#env *)
+ (** @param env disambiguation environment. If this parameter is given the
+ * disambiguator act statelessly, that is internal disambiguation status
+ * want be changed but only returned. If this parameter is not given the
+ * internal one will be used and updated with the disambiguation status
+ * resulting from the disambiguation *)
method disambiguateTerm:
?context:Cic.context -> ?metasenv:Cic.metasenv ->
?env:DisambiguateTypes.environment ->
char Stream.t ->
(DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+ (** @param env @see disambiguateTerm above *)
method disambiguateTermAst:
?context:Cic.context -> ?metasenv:Cic.metasenv ->
?env:DisambiguateTypes.environment ->
method setStatus: proofStatus -> unit
end
+ (** interpreter for toplevel phrases given via console *)
+class type interpreter =
+ object
+ method evalPhrase: string -> unit
+ end
+
(** {2 shorthands} *)
type namer = ProofEngineTypes.mk_fresh_name_type
projects / helm.git / commitdiff