filled toolbar and implemented buttons behaviours

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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 3e505c28e1b1b18bdcfc35171100b79567cc0413..d5ca65d22bebddf4dddaf3aa131bc807e1703b93 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
@@ -187,28 +188,26 @@ class proofState
     | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
     | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
         PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
-    | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac
-    | TacticAst.Assumption -> VariousTactics.assumption_tac
-    | TacticAst.Contradiction -> NegationTactics.contradiction_tac
-    | TacticAst.Exists -> IntroductionTactics.exists_tac
-    | TacticAst.Fourier -> FourierR.fourier_tac
-    | TacticAst.Left -> IntroductionTactics.left_tac
-    | TacticAst.Right -> IntroductionTactics.right_tac
-    | TacticAst.Ring -> Ring.ring_tac
-    | TacticAst.Split -> IntroductionTactics.split_tac
-    | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
-    | TacticAst.Transitivity term ->
-        EqualityTactics.transitivity_tac (disambiguate term)
-    | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
-    | TacticAst.Absurd term -> NegationTactics.absurd_tac (disambiguate term)
-    | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
-    | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
+    | TacticAst.Reflexivity -> Tactics.reflexivity
+    | TacticAst.Assumption -> Tactics.assumption
+    | TacticAst.Contradiction -> Tactics.contradiction
+    | TacticAst.Exists -> Tactics.exists
+    | TacticAst.Fourier -> Tactics.fourier
+    | TacticAst.Left -> Tactics.left
+    | TacticAst.Right -> Tactics.right
+    | TacticAst.Ring -> Tactics.ring
+    | TacticAst.Split -> Tactics.split
+    | TacticAst.Symmetry -> Tactics.symmetry
+    | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term)
+    | TacticAst.Apply term -> Tactics.apply (disambiguate term)
+    | TacticAst.Absurd term -> Tactics.absurd (disambiguate term)
+    | TacticAst.Exact term -> Tactics.exact (disambiguate term)
+    | TacticAst.Cut term -> Tactics.cut (disambiguate term)
     | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
-        PrimitiveTactics.elim_intros_simpl_tac (disambiguate term)
-    | TacticAst.ElimType term ->
-        EliminationTactics.elim_type_tac (disambiguate term)
+        Tactics.elim_intros_simpl (disambiguate term)
+    | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term)
     | TacticAst.Replace (what, with_what) ->
-        EqualityTactics.replace_tac ~what:(disambiguate what)
+        Tactics.replace ~what:(disambiguate what)
           ~with_what:(disambiguate with_what)
   (*
     (* TODO Zack a lot more of tactics to be implemented here ... *)
@@ -285,19 +284,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