974 \isacommand{imports}~@{text Main}\\ |
974 \isacommand{imports}~@{text Main}\\ |
975 \isacommand{begin}\\ |
975 \isacommand{begin}\\ |
976 \isacommand{ML}~@{text "\<verbopen>"}\\ |
976 \isacommand{ML}~@{text "\<verbopen>"}\\ |
977 @{ML |
977 @{ML |
978 "let |
978 "let |
979 val do_nothing = Scan.succeed (LocalTheory.theory I) |
979 val do_nothing = Scan.succeed (Local_Theory.theory I) |
980 val kind = OuterKeyword.thy_decl |
980 val kind = OuterKeyword.thy_decl |
981 in |
981 in |
982 OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing |
982 OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing |
983 end"}\\ |
983 end"}\\ |
984 @{text "\<verbclose>"}\\ |
984 @{text "\<verbclose>"}\\ |
1091 printing this proposition inside the tracing buffer. |
1091 printing this proposition inside the tracing buffer. |
1092 |
1092 |
1093 The crucial part of a command is the function that determines the behaviour |
1093 The crucial part of a command is the function that determines the behaviour |
1094 of the command. In the code above we used a ``do-nothing''-function, which |
1094 of the command. In the code above we used a ``do-nothing''-function, which |
1095 because of @{ML_ind succeed in Scan} does not parse any argument, but immediately |
1095 because of @{ML_ind succeed in Scan} does not parse any argument, but immediately |
1096 returns the simple function @{ML "LocalTheory.theory I"}. We can |
1096 returns the simple function @{ML "Local_Theory.theory I"}. We can |
1097 replace this code by a function that first parses a proposition (using the |
1097 replace this code by a function that first parses a proposition (using the |
1098 parser @{ML OuterParse.prop}), then prints out the tracing |
1098 parser @{ML OuterParse.prop}), then prints out the tracing |
1099 information (using a new function @{text trace_prop}) and |
1099 information (using a new function @{text trace_prop}) and |
1100 finally does nothing. For this you can write: |
1100 finally does nothing. For this you can write: |
1101 *} |
1101 *} |
1102 |
1102 |
1103 ML{*let |
1103 ML{*let |
1104 fun trace_prop str = |
1104 fun trace_prop str = |
1105 LocalTheory.theory (fn ctxt => (tracing str; ctxt)) |
1105 Local_Theory.theory (fn ctxt => (tracing str; ctxt)) |
1106 |
1106 |
1107 val kind = OuterKeyword.thy_decl |
1107 val kind = OuterKeyword.thy_decl |
1108 in |
1108 in |
1109 OuterSyntax.local_theory "foobar_trace" "traces a proposition" |
1109 OuterSyntax.local_theory "foobar_trace" "traces a proposition" |
1110 kind (OuterParse.prop >> trace_prop) |
1110 kind (OuterParse.prop >> trace_prop) |
1179 done |
1179 done |
1180 |
1180 |
1181 text {* |
1181 text {* |
1182 {\bf TBD below} |
1182 {\bf TBD below} |
1183 |
1183 |
1184 (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory}) |
1184 (FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory}) |
1185 |
1185 |
1186 *} |
1186 *} |
1187 |
1187 |
1188 ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*} |
1188 ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*} |
1189 ML{*let |
1189 ML{*let |
1190 fun after_qed thm_name thms lthy = |
1190 fun after_qed thm_name thms lthy = |
1191 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
1191 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
1192 |
1192 |
1193 fun setup_proof (thm_name, (txt, pos)) lthy = |
1193 fun setup_proof (thm_name, (txt, pos)) lthy = |
1194 let |
1194 let |
1195 val trm = ML_Context.evaluate lthy true ("r", r) txt |
1195 val trm = ML_Context.evaluate lthy true ("r", r) txt |
1196 in |
1196 in |