buildTimeConf.cmx matitaMathView.cmi
matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi
-matita.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi matitaMathView.cmi \
- matitaInterpreter.cmi matitaGui.cmi matitaGtkMisc.cmi \
+matita.cmo: matitaTypes.cmi matitaScript.cmi matitaProof.cmi matitaMisc.cmi \
+ matitaMathView.cmi matitaInterpreter.cmi matitaGui.cmi matitaGtkMisc.cmi \
matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo
-matita.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx matitaMathView.cmx \
- matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \
+matita.cmx: matitaTypes.cmx matitaScript.cmx matitaProof.cmx matitaMisc.cmx \
+ matitaMathView.cmx matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \
matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx
matitaProof.cmo: matitaTypes.cmi matitaMisc.cmi matitaCicMisc.cmi \
buildTimeConf.cmo matitaProof.cmi
matitaProof.cmx: matitaTypes.cmx matitaMisc.cmx matitaCicMisc.cmx \
buildTimeConf.cmx matitaProof.cmi
+matitaScript.cmo: matitaTypes.cmi matitaMisc.cmi matitaMathView.cmi \
+ matitaGui.cmi matitaScript.cmi
+matitaScript.cmx: matitaTypes.cmx matitaMisc.cmx matitaMathView.cmx \
+ matitaGui.cmx matitaScript.cmi
matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmi
matitaTypes.cmx: buildTimeConf.cmx matitaTypes.cmi
matitaCicMisc.cmi: matitaTypes.cmi
matitaInterpreter.cmi: matitaTypes.cmi
matitaMathView.cmi: matitaTypes.cmi
matitaProof.cmi: matitaTypes.cmi
+matitaScript.cmi: matitaTypes.cmi matitaGeneratedGui.cmi
matitaProof.cmo \
matitaDisambiguator.cmo \
matitaMathView.cmo \
- matitaInterpreter.cmo
+ matitaInterpreter.cmo \
+ matitaScript.cmo
# objects for matitac (batch compiler)
CCMOS = \
buildTimeConf.cmo \
ignore (GMain.Main.init ())
let gui = MatitaGui.instance ()
+let disambiguator = MatitaDisambiguator.instance ()
let _ = (* set disambiguator callbacks *)
- let disambiguator = MatitaDisambiguator.instance () in
disambiguator#setChooseUris (interactive_user_uri_choice ~gui);
disambiguator#setChooseInterp (interactive_interp_choice ~gui)
+
let _ = (* environment trust *)
CicEnvironment.set_trust
(let trust = Helm_registry.get_bool "matita.environment_trust" in
let currentProof = MatitaProof.instance ()
-
-let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
-let sequents_viewer =
- let set_goal goal =
- if not (currentProof#onGoing ()) then assert false;
- currentProof#proof#set_goal goal
- in
- MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
- ~sequent_viewer ~set_goal ()
+let sequent_viewer = MatitaMathView.sequent_viewer_instance ()
+let sequents_viewer = MatitaMathView.sequents_viewer_instance ()
let _ = (* attach observers to proof status *)
let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
let interpreter =
let mathViewer = MatitaMathView.mathViewer () in
MatitaInterpreter.interpreter ~console:gui#console ~mathViewer ()
+let script = MatitaScript.script ~interpreter
let _ =
let href_callback uri =
let term = CicAst.Uri (uri, None) in
in
sequent_viewer#set_href_callback (Some href_callback)
-(** {2 Script window handling} *)
-
-let script_forward _ =
- let buf = gui#script#scriptTextView#buffer in
- let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
- let (success, hide) =
- interpreter#evalPhrase
- (buf#get_text ~start:locked_iter ~stop:buf#end_iter ())
+let console_callback s =
+ let module A = TacticAst in
+ let rec strip_locations = function
+ | A.LocatedTactical (loc, tac) -> strip_locations tac
+ | tac -> tac
in
- if success then
- gui#lockScript (locked_iter#offset + interpreter#endOffset)
-
-let script_jump _ =
- let buf = gui#script#scriptTextView#buffer in
- let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
- let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
- let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in
- let len = String.length raw_text in
- let rec parse offset =
- if offset < len then begin
- let (success, hide) =
- interpreter#evalPhrase (String.sub raw_text offset (len - offset))
- in
- if success then begin
- let new_offset = interpreter#endOffset + offset in
- gui#lockScript (new_offset + locked_iter#offset);
- parse new_offset
- end else
- raise Exit
- end
+ let needed_by_script ast =
+ prerr_endline (TacticAstPp.pp_tactical ast);
+ match strip_locations ast with
+ | A.Tactic _
+ | A.Command
+ (A.Inductive _ | A.Theorem _ | A.Coercion _ | A.Qed _ | A.Proof) ->
+ true
+ | _ -> false
in
- try
- parse 0
- with Exit -> ()
+ let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in
+ if needed_by_script ast then
+ script#advance ast
+ else
+ interpreter#evalAst ast
-let script_back _ = not_implemented "script_back"
-
-let load_script fname =
- gui#script#scriptTextView#buffer#set_text (input_file fname);
- gui#script#scriptWin#show ();
- gui#main#showScriptMenuItem#set_active true
+let console_callback s =
+ match gui#console#wrap_exn (fun () -> console_callback s) with
+ | None -> (false, false)
+ | Some outcome -> outcome
(** {2 GUI callbacks} *)
let _ =
gui#setQuitCallback currentProof#quit;
- gui#setPhraseCallback interpreter#evalPhrase;
+ gui#setPhraseCallback console_callback;
gui#main#debugMenu#misc#hide ();
ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
gui#console#clear ();
ignore (gui#main#openMenuItem#connect#activate (fun _ ->
match gui#chooseFile () with
| None -> ()
- | Some f when is_proof_script f -> load_script f
+ | Some f when is_proof_script f ->
+ ignore (gui#console#wrap_exn (fun () -> script#loadFrom f))
| Some f ->
gui#console#echo_error (sprintf
"Don't know what to do with file: %s\nUnrecognized file format."
f)));
ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
ignore (MatitaMathView.cicBrowser ())));
- connect_button gui#script#scriptWinForwardButton script_forward;
- connect_button gui#script#scriptWinBackButton script_back;
- connect_button gui#script#scriptWinJumpButton script_jump;
let module A = TacticAst in
let hole = CicAst.UserInput in
- let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in
+ let tac ast _ =
+ let ast = A.Tactic ast in
+ ignore (interpreter#evalAst ast);
+ ignore (script#advance ast)
+ in
let tac_w_term ast _ =
(* gui#console#clear (); *)
gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
(** </DEBUGGING> *)
let _ =
-(*
- (try
- load_script Sys.argv.(1)
- with Invalid_argument _ -> ());
-*)
+ (try script#loadFrom Sys.argv.(1) with Invalid_argument _ -> ());
if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
Helm_registry.set "matita.mode" "cicbrowser";
let browser = MatitaMathView.cicBrowser () in
class virtual interpreterState =
(* static values, shared by all states inheriting this class *)
let loc = ref None in
- let history = ref [] in
+ let last_item = ref None in
+ let evalAstCallback = ref None in
fun ~(console: #MatitaTypes.console) ->
object (self)
(** eval a toplevel phrase in the current state and return the new state
*)
method parsePhrase s =
- match CicTextualParser2.parse_tactical s with
+ match disambiguator#parserr#parseTactical s with
| (TacticAst.LocatedTactical (loc', tac)) as tactical ->
loc := Some loc';
- (match tac with (* update interpreter history *)
- | TacticAst.Command (TacticAst.Qed None) ->
- history := `Qed :: !history
- | TacticAst.Command (TacticAst.Theorem (_, Some name, _, None)) ->
- history := `Theorem name :: !history
- | TacticAst.Command (TacticAst.Qed _)
- | TacticAst.Command (TacticAst.Theorem _) -> assert false
- | _ -> history := `Tactic :: !history);
tactical
| _ -> assert false
method virtual evalTactical:
(CicAst.term, string) TacticAst.tactical -> outcome
+ method private _evalTactical ast =
+ self#setLastItem None;
+ let res = self#evalTactical ast in
+ (match !evalAstCallback with Some f -> f ast | None -> ());
+ res
+
method evalPhrase s =
debug_print (sprintf "evaluating '%s'" s);
- self#evalTactical (self#parsePhrase (Stream.of_string s))
+ self#_evalTactical (self#parsePhrase (Stream.of_string s))
- method evalAst ast = self#evalTactical ast
+ method evalAst ast = self#_evalTactical ast
method endOffset =
match !loc with
| Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum
| None -> failwith "MatitaInterpreter: no offset recorded"
+ method lastItem: script_item option = !last_item
+ method private setLastItem item = last_item := item
+
+ method setEvalAstCallback f = evalAstCallback := Some f
+
end
(** Implements phrases that should be accepted in all states *)
let uri = UriManager.uri_of_string (qualify name ^ ".con") in
let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in
currentProof#start proof;
+ self#setLastItem (Some `Theorem);
New_state Proof
| TacticAst.Command
(TacticAst.Theorem (_, Some name, type_ast, Some body_ast)) ->
let body = CicMetaSubst.apply_subst subst body_cic in
let ty = CicMetaSubst.apply_subst subst type_cic in
add_constant_to_world ~console ~dbd ~uri ~body ~ty ~ugraph ();
+ self#setLastItem (Some (`Def uri));
Quiet
| TacticAst.Command (TacticAst.Inductive (params, indTypes)) ->
in
add_inductive_def_to_world ~console
~dbd ~uri ~indTypes ~params ~leftno ~ugraph ();
+ self#setLastItem (Some (`Inductive uri));
Quiet
| TacticAst.Command TacticAst.Quit ->
currentProof#quit ();
UriManager.uri_of_string (base ^ xp)
| Cic.Appl (he::_) -> uri_of_term he
| t ->
- prerr_endline ("Fallisco a estrarre la uri di " ^
- (CicPp.ppterm t));
+ error ("can't extract uri from " ^ (CicPp.ppterm t));
assert false
in
let ty_src,ty_tgt = extract_last_two_p coer_ty in
add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph ();
currentProof#abort ();
console#echo_message (sprintf "%s defined" suri);
+ self#setLastItem (Some (`Qed uri));
New_state Command
| TacticAst.Seq tacticals ->
- (* TODO Zack check for proof completed at each step? *)
+ (* TODO ZACK check for proof completed at each step? *)
+ (* TODO ZACK code completely broken here: we must build logic level
+ * tacticals instead of iterating interpreter evaluation *)
+ if (List.length tacticals > 1) then
+ warning "tacticals are broken: see matitaInterpreter.ml";
List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
+ self#setLastItem (Some `Tactic);
New_state Proof
| TacticAst.Tactic tactic_phrase ->
let tactic = self#lookup_tactic tactic_phrase in
currentProof#proof#apply_tactic tactic;
+ self#setLastItem (Some `Tactic);
New_state Proof
| tactical -> shared#evalTactical tactical
end
object (self)
val mutable state = commandState
- method reset = state <- commandState
-
- method endOffset = state#endOffset
+ method setState (tag: [`Proof | `Command]) =
+ match tag with
+ | `Proof -> (state <- proofState)
+ | `Command -> (state <- commandState)
method private updateState = function
| New_state Command -> (state <- commandState)
method evalPhrase s = self#eval (fun () -> state#evalPhrase s)
method evalAst ast = self#eval (fun () -> state#evalAst ast)
+
+ (** {2 methods delegated to current state} *)
+
+ method endOffset = state#endOffset
+ method lastItem = state#lastItem
+ method setEvalAstCallback = state#setEvalAstCallback
end
let interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
--- /dev/null
+(* Copyright (C) 2005, 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
+
+exception Script_failure of string
+
+let remove_constant_from_world ~dbd ~uri =
+ CicEnvironment.remove_obj uri;
+ MetadataDb.unindex ~dbd ~uri;
+ let uri = UriManager.string_of_uri uri in
+ List.iter
+ (* TODO ZACK remove xml files from disk *)
+ (fun suffix -> Http_getter.unregister (uri ^ suffix))
+ [""; ".body"; ".types"]
+
+let remove_inductive_def_from_world ~dbd ~uri =
+ remove_constant_from_world ~dbd ~uri;
+ let uri = UriManager.string_of_uri uri in
+ Http_getter.unregister uri;
+ List.iter
+ (fun suffix ->
+ let uri =
+ Pcre.replace ~pat:"\\.ind$" ~templ:(sprintf "_%s.con" suffix) uri
+ in
+ remove_constant_from_world ~dbd ~uri:(UriManager.uri_of_string uri))
+ ["ind"; "rec"; "rect"]
+
+let is_empty =
+ let rex = Pcre.regexp "^\\s*$" in
+ fun s ->
+ Pcre.pmatch ~rex s
+
+class script ~(interpreter:MatitaTypes.interpreter) () =
+ let gui = MatitaGui.instance () in
+ let script = gui#script in
+ let buf = script#scriptTextView#buffer in
+ let dbd = MatitaMisc.dbd_instance () in
+ let rec undo_item = function
+ | None -> ()
+ | Some item ->
+ (match item with
+ | `Tactic ->
+ let res =
+ interpreter#evalAst (TacticAst.Command (TacticAst.Undo None))
+ in
+ assert (fst res)
+ | `Theorem ->
+ interpreter#setState `Command;
+ (MatitaMathView.sequents_viewer_instance ())#reset
+ | `Qed uri
+ | `Def uri -> remove_constant_from_world ~dbd ~uri
+ | `Inductive uri -> remove_inductive_def_from_world ~dbd ~uri)
+ in
+ object (self)
+ initializer
+ let console = (MatitaGui.instance ())#console in
+ let w f () = ignore (console#wrap_exn (fun () -> f ())) in
+ ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top));
+ ignore (gui#script#scriptWinBottomButton#connect#clicked (w self#bottom));
+ ignore (gui#script#scriptWinForwardButton#connect#clicked
+ (w self#forward));
+ ignore (gui#script#scriptWinBackButton#connect#clicked (w self#back));
+ ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top));
+ ignore (gui#script#scriptWinJumpButton#connect#clicked (w self#jump))
+
+ val mutable items = []
+
+ (** {3 text buffer locking} *)
+
+ (** text mark and tag representing locked part of a script *)
+ val locked_mark =
+ buf#create_mark ~name:"locked" ~left_gravity:true buf#start_iter
+ val locked_tag = buf#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
+
+ (** lock script text view from the beginning to the given offset (in UTF-8
+ * characters) *)
+ method private lockScript offset =
+ let mark = `MARK locked_mark in
+ buf#move_mark mark ~where:(buf#get_iter_at_char offset);
+ buf#remove_tag locked_tag ~start:buf#start_iter ~stop:buf#end_iter;
+ buf#apply_tag locked_tag ~start:buf#start_iter
+ ~stop:(buf#get_iter_at_mark mark)
+
+ method win = gui#script
+
+ method loadFrom fname =
+ buf#set_text (MatitaMisc.input_file fname);
+ gui#script#scriptWin#show ();
+ gui#main#showScriptMenuItem#set_active true
+
+ method advance tactical =
+ let text = "\n" ^ TacticAstPp.pp_tactical tactical in
+ buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) text;
+ let res = self#_forward () in
+ if not (fst res) then begin
+ let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+ buf#delete ~start:locked_iter
+ ~stop:(locked_iter#forward_chars (String.length text));
+ end;
+ res
+
+ (** {3 script progress} *)
+
+ method private jump () =
+ let locked_iter () = buf#get_iter_at_mark (`NAME "locked") in
+ let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
+ let rec forward_until_cursor () =
+ prerr_endline "forward_until_cursor";
+ (* go forward until locked > cursor (or forward fails) *)
+ let success =
+ try
+ fst (self#_forward ~stop:cursor_iter ())
+ with
+ | Script_failure _ | CicTextualParser2.Parse_error _ -> false
+ in
+ if success && (locked_iter ())#compare cursor_iter < 0 then
+ forward_until_cursor ()
+ in
+ let rec back_until_cursor () = (* go backward until locked < cursor *)
+ prerr_endline "back_until_cursor";
+ let res = self#back () in
+ if (locked_iter ())#compare cursor_iter > 0 then
+ back_until_cursor ()
+ in
+ let cmp = (locked_iter ())#compare cursor_iter in
+ if cmp < 0 then (* locked < cursor *)
+ (prerr_endline "locked < cursor"; forward_until_cursor ())
+ else if cmp > 0 then (* locked > cursor *)
+ (prerr_endline "locked > cursor"; back_until_cursor ())
+ else (* cursor = locked *)
+ ()
+
+ method private top () =
+ try while true do self#back () done with Script_failure _ -> ()
+
+ method private bottom () =
+ try
+ while true do
+ let res = self#_forward () in
+ if not (fst res) then raise (Script_failure "error")
+ done
+ with Script_failure _ -> ()
+
+ method private _forward ?(stop = buf#end_iter) () =
+ let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+ let (success, hide) as res =
+ let text = buf#get_text ~start:locked_iter ~stop () in
+ if is_empty text then
+ raise (Script_failure "at bottom")
+ else
+ interpreter#evalPhrase text
+ in
+ if success then begin
+ let old_offset = locked_iter#offset in
+ let new_offset = old_offset + interpreter#endOffset in
+ self#lockScript new_offset;
+ items <- (interpreter#lastItem, old_offset) :: items
+ end;
+ res
+
+ method private forward () = ignore (self#_forward ())
+
+ method private back () =
+ (* clean history backward until the first theorem, return offset before
+ * it and remaning history *)
+ let rec flush_theorem = function
+ | (Some `Theorem, offset) :: tl -> offset, tl
+ | _ :: tl -> flush_theorem tl
+ | [] -> assert false
+ in
+ match items with
+ | [] -> raise (Script_failure "at top")
+ | (item, last_offset) :: tl ->
+ undo_item item;
+ let (last_offset, tl) =
+ (* if undoing a qed, go back before corresponding theorem *)
+ match item with
+ | Some (`Qed _) -> flush_theorem tl
+ | _ -> last_offset, tl
+ in
+ items <- tl;
+ self#lockScript last_offset
+
+ end
+
+let script ~interpreter = new script ~interpreter ()
+
--- /dev/null
+(* Copyright (C) 2005, 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/
+ *)
+
+ (** script failures (e.g. going before the beginning or after the end of the
+ * script) *)
+exception Script_failure of string
+
+class type script =
+ object
+ (** script window used by this script *)
+ method win: MatitaGeneratedGui.scriptWin
+
+ (** fill text buffer reading a script from a file *)
+ method loadFrom: string -> unit
+
+ (** adds a tactical at current script execution point and execute it. Used
+ * when the user uses buttons or console instead of directly editing the
+ * script *)
+ method advance: DisambiguateTypes.tactical -> MatitaTypes.command_outcome
+ end
+
+val script: interpreter:MatitaTypes.interpreter -> script
+
type command_outcome = bool * bool
+type script_item =
+ [ `Tactic
+ | `Theorem
+ | `Qed of UriManager.uri
+ | `Def of UriManager.uri
+ | `Inductive of UriManager.uri
+ ]
+
class type interpreter =
object
- method endOffset : int
method evalAst : DisambiguateTypes.tactical -> command_outcome
method evalPhrase : string -> command_outcome
(* method evalStream: char Stream.t -> command_outcome *)
- method reset : unit
+ method endOffset : int
+ method lastItem: script_item option
+ method setState: [`Proof | `Command] -> unit
+ method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
end
type term_source =
* second component represents console action: true = hide, false = keep *)
type command_outcome = bool * bool
+ (** schematic representation of items scripts are made of *)
+type script_item =
+ [ `Tactic (** action on proof status *)
+ | `Theorem (** start of proof, to be proved *)
+ | `Qed of UriManager.uri (** end of proof, successfull *)
+ | `Def of UriManager.uri (** constant with body *)
+ | `Inductive of UriManager.uri (** inductive definition *)
+ ]
+
(** interpreter for toplevel phrases given via console *)
class type interpreter =
object
- method reset: unit (** return the interpreter to the initial state *)
-
(** parse a single phrase contained in the input string. Additional
* garbage at the end of the phrase is ignored
* @return true if no exception has been raised by the evaluation, false
(** as above, evaluating a command/tactics AST *)
method evalAst: DisambiguateTypes.tactical -> command_outcome
+ (** {3 callbacks} *)
+
+ method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
+
+ (** {3 stateful methods}
+ * bookkeeping of last interpreted phrase *)
+
(** offset from the starting of the last string parser by evalPhrase where
* parsing stop.
* @raise Failure when no offset has been recorded *)
method endOffset: int
+ (** last item parsed *)
+ method lastItem: script_item option
+
+ (** change internal interpreter state *)
+ method setState: [`Proof | `Command] -> unit
+
end
(** {2 MathML widgets} *)
projects / helm.git / commitdiff