# HG changeset patch
# User wenzelm
# Date 1427976660 -7200
# Node ID fbf4d5ad500d2ab735f441f9315ba8f130a923ab
# Parent  fdf6957f86355350c32961c0e951a68207438605
clarified method_closure;
added option for Eisbach, which makes its own closure;

diff -r fdf6957f8635 -r fbf4d5ad500d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Apr 02 12:24:30 2015 +0200
+++ b/src/Pure/Isar/method.ML	Thu Apr 02 14:11:00 2015 +0200
@@ -65,6 +65,7 @@
   val method_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory
   val method: Proof.context -> Token.src -> Proof.context -> method
   val method_closure: Proof.context -> Token.src -> Token.src
+  val closure: bool Config.T
   val method_cmd: Proof.context -> Token.src -> Proof.context -> method
   val evaluate: text -> Proof.context -> method
   type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
@@ -395,15 +396,19 @@
   let val table = get_methods (Context.Proof ctxt)
   in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
 
-fun method_closure ctxt0 src0 =
+fun method_closure ctxt src =
   let
-    val src1 = check_src ctxt0 src0;
-    val src2 = Token.init_assignable_src src1;
-    val ctxt = Context_Position.not_really ctxt0;
-    val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
-  in Token.closure_src src2 end;
+    val src' = Token.init_assignable_src src;
+    val ctxt' = Context_Position.not_really ctxt;
+    val _ = Seq.pull (method ctxt' src' ctxt' [] (Goal.protect 0 Drule.dummy_thm));
+  in Token.closure_src src' end;
 
-fun method_cmd ctxt = method ctxt o method_closure ctxt;
+val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true)));
+
+fun method_cmd ctxt =
+  check_src ctxt #>
+  Config.get ctxt closure ? method_closure ctxt #>
+  method ctxt;
 
 
 (* evaluate method text *)