snapshot, notably:

[helm.git] / helm / matita / matitaInterpreter.ml

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 3e505c28e1b1b18bdcfc35171100b79567cc0413..17a055174d91507fdd60c9b6f15a8b2af7b21f48 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -84,6 +84,7 @@ class virtual interpreterState ~(console: MatitaConsole.console) =
       (CicAst.term, string) TacticAst.tactical -> state_tag
 
     method evalPhrase s = self#evalTactical (self#parsePhrase s)
+
   end
 
 let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy
@@ -285,19 +286,39 @@ class interpreter
     new commandState ~disambiguator ~proof_handler ~console ()
   in
   let proofState = new proofState ~disambiguator ~proof_handler ~console () in
-  object
+  object (self)
     val mutable state = commandState
 
     method reset = state <- commandState
 
+    method private updateState = function
+      | Some `Command -> state <- commandState
+      | Some `Proof -> state <- proofState
+      | None -> ()
+
     method evalPhrase s =
       try
-        (match state#evalPhrase s with
-        | Some `Command -> state <- commandState
-        | Some `Proof -> state <- proofState
-        | None -> ())
+        self#updateState (state#evalPhrase s)
       with exn ->
         console#echo_error (sprintf "Uncaught exception: %s"
           (Printexc.to_string exn))
+
+(*
+    method evalAll s =
+      let get_end_pos = function
+        | TacticAst.LocatedTactical ((_, end_pos), _) -> end_pos.Lexing.pos_cnum
+        | _ -> assert false
+      in
+      let str_len = String.length s in
+      let rec aux offset =
+        let tactical =
+          self#parsePhrase (String.sub s offset (str_len - offset))
+        in
+        self#updateState (state#evalTactical tactical);
+        let next_offset = get_end_pos tactical + offset in
+        if next_offset = str_len - 1 then
+      in
+*)
+
   end