isabelle-cookbook: ProgTutorial/Base.thy@5accec94b6df (annotated)

23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	1	theory Base
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	2	imports Main
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	3	uses
256 1fb8d62c88a0 added some first index-information Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	4	"output_tutorial.ML"
57 065f472c09ab Repaired output of marginal comments in ML antiquotation. berghofe parents: 43 diff changeset	5	"chunks.ML"
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	6	"antiquote_setup.ML"
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	7	begin
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	8
64 9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	9	(* to have a special tag for text enclosed in ML *)
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	10	ML {*
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	11
260 5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	12	fun propagate_env (context as Context.Proof lthy) =
5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	13	Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	14	\| propagate_env context = context;
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	15
260 5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	16	fun propagate_env_prf prf = Proof.map_contexts
5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	17	(Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	18
64 9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	19	val _ =
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	20	OuterSyntax.command "ML" "eval ML text within theory"
106 bdd82350cf22 renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious) Christian Urban <urbanc@in.tum.de> parents: 80 diff changeset	21	(OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
64 9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	22	(OuterParse.ML_source >> (fn (txt, pos) =>
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	23	Toplevel.generic_theory
260 5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	24	(ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	25
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	26	val _ =
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	27	OuterSyntax.command "ML_prf" "ML text within proof"
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	28	(OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	29	(OuterParse.ML_source >> (fn (txt, pos) =>
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	30	Toplevel.proof (Proof.map_context (Context.proof_map
260 5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	31	(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	32
224 647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	33	val _ =
647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	34	OuterSyntax.command "ML_val" "diagnostic ML text"
647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	35	(OuterKeyword.tag "TutorialML" OuterKeyword.diag)
647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	36	(OuterParse.ML_source >> IsarCmd.ml_diag true);
647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	37
64 9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	38	*}
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	39
255 ef1da1abee46 added infrastructure for index; antiquotations have now the options [index] and [indexc] Christian Urban <urbanc@in.tum.de> parents: 239 diff changeset	40
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	41	end

author	Christian Urban <urbanc@in.tum.de>
	Fri, 05 Jun 2009 04:17:28 +0200
changeset 260	5accec94b6df
parent 256	1fb8d62c88a0
child 264	311830b43f8f
permissions	-rw-r--r--