1092 

  1092 (*

  1093 

  1093 ML {*

  1094 structure TacticData = ProofDataFun

  1095 (

  1096   type T = thm list -> tactic;

  1097   fun init _ = undefined;

  1098 );

  1099 

  1100 val set_tactic = TacticData.put;

  1101 *}

  1102 

  1103 ML {*

  1104   TacticData.get @{context}

  1105 *}

  1106 

  1107 ML {* Method.set_tactic  *}

  1108 ML {* fun tactic (facts: thm list) : tactic = (atac 1) *}

  1109 ML {* Context.map_proof *}

  1110 ML {* ML_Context.expression *}

  1111 ML {* METHOD *}

  1112 

  1113 

  1114 ML {* 

  1115 fun myexpression pos bind body txt =

  1116 let

  1117   val _ = tracing ("bind)" ^ bind)

  1118   val _ = tracing ("body)" ^ body)

  1119   val _ = tracing ("txt)"  ^ txt)

  1120   val _ = tracing ("result) " ^ "Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^

  1121       " end (ML_Context.the_generic_context ())));")

  1122 in

  1123   ML_Context.exec (fn () => ML_Context.eval false pos

  1124     ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^

  1125       " end (ML_Context.the_generic_context ())));"))

  1126 end

  1127 *}

  1128 

  1129 

  1130 ML {*

  1131 fun ml_tactic (txt, pos) ctxt =

  1132 let

  1133   val ctxt' = ctxt |> Context.proof_map

  1134       (myexpression pos

  1135         "fun tactic (facts: thm list) : tactic"

  1136         "Context.map_proof (Method.set_tactic tactic)" txt);

  1137 in 

  1138   Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt')

  1139 end;

  1140 *}

  1141 

  1142 ML {*

  1143 fun tactic3 (txt, pos) ctxt = 

  1144   let

  1145     val _ = tracing ("1) " ^ txt )

  1146   in 

  1147    METHOD (ml_tactic (txt, pos) ctxt; K (atac 1))

  1148   end

  1149 *}

  1150 

  1151 setup {*

  1152 Method.setup (Binding.name "tactic3") (Scan.lift (OuterParse.position Args.name) 

  1153   >> tactic3)

  1154     "ML tactic as proof method"

  1155 *}

  1156 

  1157 lemma "A \<Longrightarrow> A"

  1158 apply(tactic3 {* (atac 1)  *})

  1159 done

  1160 

  1161 ML {* 

  1162 (ML_Context.the_generic_context ())

  1163 *}

  1164 

  1165 ML {*

  1166 Context.set_thread_data;

  1167 ML_Context.the_generic_context

  1168 *}

  1169 

  1170 lemma "A \<Longrightarrow> A"

  1171 ML_prf {*

  1172 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 ())));

  1173 *}

  1174 

  1175 ML {*

  1176 Context.set_thread_data (SOME ((let fun tactic (facts: thm list) : tactic =  (atac 1)   in 3 end) (ML_Context.the_generic_context ())));

  1177 *}

  1178 

  1179 ML {*

  1180 Context.set_thread_data (SOME (let 

  1181   fun tactic (facts: thm list) : tactic =  (atac 1) 

  1182 in 

  1183   Context.map_proof (Method.set_tactic tactic) 

  1184 end 

  1185   (ML_Context.the_generic_context ())));

  1186 *}

  1187 

  1188 

  1189 ML {*

  1190 let 

  1191   fun tactic (facts: thm list) : tactic = atac

  1192 in

  1193   Context.map_proof (Method.set_tactic tactic)

  1194 end *}

  1195 

  1196 end *}

  1197 

  1198 ML {* Toplevel.program (fn () => 

  1199 (ML_Context.expression Position.none "val plus : int" "3 + 4" "1" (Context.Proof @{context})))*}

  1200 

  1201 

  1202 ML {*

  1203 fun ml_tactic (txt, pos) ctxt =

  1204   let

  1205     val ctxt' = ctxt |> Context.proof_map

  1206       (ML_Context.expression pos

  1207         "fun tactic (facts: thm list) : tactic"

  1208         "Context.map_proof (Method.set_tactic tactic)" txt);

  1209   in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;

  1210 

  1211 *}

  1212 

  1213 ML {*

  1214 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 ())));

  1215 *}

  1216 *)