--- a/ProgTutorial/FirstSteps.thy	Sat Aug 22 02:56:08 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Aug 25 00:07:37 2009 +0200
@@ -179,7 +179,7 @@
   @{ML_ind  profiling in Toplevel}.)
 *}
 
-(*
+(* FIXME
 ML {* reset Toplevel.debug *}
 
 ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}
@@ -831,4 +831,18 @@
   own document antiquotations. 
 *}
 
+(*
+section {* Do Not Try This At Home! *}
+
+ML {* val my_thms = ref ([]: thm list) *}
+
+attribute_setup my_thm_bad =
+  {* Scan.succeed (Thm.declaration_attribute (fn th => fn ctxt =>
+      (my_thms := th :: ! my_thms; ctxt))) *} "bad attribute"
+
+declare sym [my_thm_bad]
+declare refl [my_thm_bad]
+
+ML "!my_thms"
+*)
 end

--- a/ProgTutorial/Parsing.thy	Sat Aug 22 02:56:08 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Tue Aug 25 00:07:37 2009 +0200
@@ -1089,8 +1089,131 @@
 apply(rule TrueI)
 done
 
+(*
+ML {*
+structure TacticData = ProofDataFun
+(
+  type T = thm list -> tactic;
+  fun init _ = undefined;
+);
+
+val set_tactic = TacticData.put;
+*}
+
+ML {*
+  TacticData.get @{context}
+*}
+
+ML {* Method.set_tactic  *}
+ML {* fun tactic (facts: thm list) : tactic = (atac 1) *}
+ML {* Context.map_proof *}
+ML {* ML_Context.expression *}
+ML {* METHOD *}
+
+
+ML {* 
+fun myexpression pos bind body txt =
+let
+  val _ = tracing ("bind)" ^ bind)
+  val _ = tracing ("body)" ^ body)
+  val _ = tracing ("txt)"  ^ txt)
+  val _ = tracing ("result) " ^ "Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
+      " end (ML_Context.the_generic_context ())));")
+in
+  ML_Context.exec (fn () => ML_Context.eval false pos
+    ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
+      " end (ML_Context.the_generic_context ())));"))
+end
+*}
 
 
+ML {*
+fun ml_tactic (txt, pos) ctxt =
+let
+  val ctxt' = ctxt |> Context.proof_map
+      (myexpression pos
+        "fun tactic (facts: thm list) : tactic"
+        "Context.map_proof (Method.set_tactic tactic)" txt);
+in 
+  Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt')
+end;
+*}
+
+ML {*
+fun tactic3 (txt, pos) ctxt = 
+  let
+    val _ = tracing ("1) " ^ txt )
+  in 
+   METHOD (ml_tactic (txt, pos) ctxt; K (atac 1))
+  end
+*}
+
+setup {*
+Method.setup (Binding.name "tactic3") (Scan.lift (OuterParse.position Args.name) 
+  >> tactic3)
+    "ML tactic as proof method"
+*}
+
+lemma "A \<Longrightarrow> A"
+apply(tactic3 {* (atac 1)  *})
+done
+
+ML {* 
+(ML_Context.the_generic_context ())
+*}
+
+ML {*
+Context.set_thread_data;
+ML_Context.the_generic_context
+*}
+
+lemma "A \<Longrightarrow> A"
+ML_prf {*
+Context.set_thread_data (SOME (let fun tactic (facts: thm list) : tactic =  (atac 1)   in Context.map_proof (Method.set_tactic tactic) end (ML_Context.the_generic_context ())));
+*}
+
+ML {*
+Context.set_thread_data (SOME ((let fun tactic (facts: thm list) : tactic =  (atac 1)   in 3 end) (ML_Context.the_generic_context ())));
+*}
+
+ML {*
+Context.set_thread_data (SOME (let 
+  fun tactic (facts: thm list) : tactic =  (atac 1) 
+in 
+  Context.map_proof (Method.set_tactic tactic) 
+end 
+  (ML_Context.the_generic_context ())));
+*}
+
+
+ML {*
+let 
+  fun tactic (facts: thm list) : tactic = atac
+in
+  Context.map_proof (Method.set_tactic tactic)
+end *}
+
+end *}
+
+ML {* Toplevel.program (fn () => 
+(ML_Context.expression Position.none "val plus : int" "3 + 4" "1" (Context.Proof @{context})))*}
+
+
+ML {*
+fun ml_tactic (txt, pos) ctxt =
+  let
+    val ctxt' = ctxt |> Context.proof_map
+      (ML_Context.expression pos
+        "fun tactic (facts: thm list) : tactic"
+        "Context.map_proof (Method.set_tactic tactic)" txt);
+  in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
+
+*}
+
+ML {*
+Context.set_thread_data (SOME (let fun tactic (facts: thm list) : tactic =  (atac 1)   in Context.map_proof (Method.set_tactic tactic) end (ML_Context.the_generic_context ())));
+*}
+*)
 
 section {* Methods (TBD) *}
 

Binary file progtutorial.pdf has changed