clarifed Method.evaluate: turn text into semantic method (like Basic);

--- a/src/Pure/Isar/method.ML	Tue Aug 19 12:05:11 2014 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 19 14:51:25 2014 +0200
@@ -69,6 +69,7 @@
     local_theory -> local_theory
   val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     local_theory -> local_theory
+  val evaluate: Proof.context -> text -> Proof.context -> method
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
@@ -389,6 +390,44 @@
   |> Context.proof_map;
 
 
+(* evaluate method text *)
+
+local
+
+fun APPEND_CASES (meth: cases_tactic) (cases, st) =
+  meth st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
+
+fun BYPASS_CASES (tac: tactic) (cases, st) =
+  tac st |> Seq.map (pair cases);
+
+val op THEN = Seq.THEN;
+
+fun SELECT_GOALS n method =
+  BYPASS_CASES
+    (ALLGOALS Goal.conjunction_tac THEN PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1)
+  THEN method
+  THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1));
+
+fun combinator comb meths ctxt facts = comb (map (fn meth => meth ctxt facts) meths);
+fun combinator1 comb meth ctxt facts = comb (meth ctxt facts);
+
+in
+
+fun evaluate static_ctxt text =
+  let
+    fun eval (Basic meth) = APPEND_CASES oo meth
+      | eval (Source src) = APPEND_CASES oo method_cmd static_ctxt src
+      | eval (Then (_, txts)) = combinator Seq.EVERY (map eval txts)
+      | eval (Orelse (_, txts)) = combinator Seq.FIRST (map eval txts)
+      | eval (Try (_, txt)) = combinator1 Seq.TRY (eval txt)
+      | eval (Repeat1 (_, txt)) = combinator1 Seq.REPEAT1 (eval txt)
+      | eval (Select_Goals (_, n, txt)) = combinator1 (SELECT_GOALS n) (eval txt);
+    val meth = eval text;
+  in fn ctxt => fn facts => fn st => meth ctxt facts ([], st) end;
+
+end;
+
+
 
 (** concrete syntax **)
 

--- a/src/Pure/Isar/proof.ML	Tue Aug 19 12:05:11 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Aug 19 14:51:25 2014 +0200
@@ -409,33 +409,11 @@
           (K (statement, [], using, goal', before_qed, after_qed)) I)
   end;
 
-fun select_goals n meth state =
-  ALLGOALS Goal.conjunction_tac (#2 (#2 (get_goal state)))
-  |> Seq.maps (fn goal =>
-    state
-    |> Seq.lift provide_goal ((PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) goal)
-    |> Seq.maps meth
-    |> Seq.maps (fn state' => state'
-      |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state')))))
-    |> Seq.maps (apply_method true (K Method.succeed)));
-
-fun apply_text current_context text state =
-  let
-    val ctxt = context_of state;
-
-    fun eval (Method.Basic m) = apply_method current_context m
-      | eval (Method.Source src) = apply_method current_context (Method.method_cmd ctxt src)
-      | eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts)
-      | eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts)
-      | eval (Method.Try (_, txt)) = Seq.TRY (eval txt)
-      | eval (Method.Repeat1 (_, txt)) = Seq.REPEAT1 (eval txt)
-      | eval (Method.Select_Goals (_, n, txt)) = select_goals n (eval txt);
-  in eval text state end;
-
 in
 
-val refine = apply_text true;
-val refine_end = apply_text false;
+fun refine text state = apply_method true (Method.evaluate (context_of state) text) state;
+fun refine_end text state = apply_method false (Method.evaluate (context_of state) text) state;
+
 fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
 
 end;