isabelle-cookbook: ProgTutorial/Base.thy@007922777ff1 (annotated)

23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	1	theory Base
264 311830b43f8f minor tuning Christian Urban <urbanc@in.tum.de> parents: 260 diff changeset	2	imports Main LaTeXsugar
23 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
302 0cbd34857b9e tuned Christian Urban <urbanc@in.tum.de> parents: 301 diff changeset	9	(* re-definition of various ML antiquotations *)
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	10	(* to have a special tag for text enclosed in ML *)
301 2728e8daebc0 replaced "writeln" with "tracing" Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	11
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	12	ML {*
310 007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	13	(* FIXME ref *)
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	14	val file_name = ref (NONE : string option)
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	15
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	16	fun write_file txt =
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	17	case !file_name of
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	18	NONE => () (* error "No open file" *)
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	19	\| SOME name =>
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	20	(let
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	21	val stream = TextIO.openAppend name
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	22	in
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	23	TextIO.output (stream, txt);
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	24	TextIO.flushOut stream;
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	25	TextIO.closeOut stream
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	26	end)
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	27	*}
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	28
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	29	ML {*
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	30	fun write_file_blk txt =
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	31	let
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	32	val pre = implode ["\n", "ML ", "{", "*", "\n"]
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	33	val post = implode ["\n", "*", "}", "\n"]
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	34	in
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	35	write_file (enclose pre post txt)
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	36	end
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	37	*}
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	38
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	39	ML {*
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	40	fun open_file name =
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	41	(tracing ("Opened File: " ^ name);
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	42	file_name := SOME name)
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	43
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	44	fun open_file_prelude name txt =
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	45	(open_file name; write_file (txt ^ "\n"))
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	46	*}
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	47
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	48
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	49	ML {*
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	50
260 5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	51	fun propagate_env (context as Context.Proof lthy) =
5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	52	Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
264 311830b43f8f minor tuning Christian Urban <urbanc@in.tum.de> parents: 260 diff changeset	53	\| propagate_env context = context
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	54
260 5accec94b6df updated to lates Isabelle changes Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	55	fun propagate_env_prf prf = Proof.map_contexts
264 311830b43f8f minor tuning Christian Urban <urbanc@in.tum.de> parents: 260 diff changeset	56	(Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
310 007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	57	*}
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	58
310 007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	59	ML {*
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	60	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	61	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	62	(OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
310 007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	63	(OuterParse.position OuterParse.text >> (fn (txt, pos) =>
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	64	Toplevel.generic_theory
310 007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	65	(ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env)))
007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	66	*}
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	67
310 007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	68	ML {*
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	69	val _ =
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	70	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	71	(OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	72	(OuterParse.ML_source >> (fn (txt, pos) =>
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	73	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	74	(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))
310 007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	75	*}
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	76
310 007922777ff1 added some rudimentary inrastructure for producing the ML-code Christian Urban <urbanc@in.tum.de> parents: 302 diff changeset	77	ML {*
224 647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	78	val _ =
647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	79	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	80	(OuterKeyword.tag "TutorialML" OuterKeyword.diag)
264 311830b43f8f minor tuning Christian Urban <urbanc@in.tum.de> parents: 260 diff changeset	81	(OuterParse.ML_source >> IsarCmd.ml_diag true)
224 647cab4a72c2 finished the heavy duty stuff for the inductive package Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	82
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	83	*}
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	84
b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	85	end

author	Christian Urban <urbanc@in.tum.de>
	Mon, 17 Aug 2009 20:57:32 +0200
changeset 310	007922777ff1
parent 302	0cbd34857b9e
child 311	ee864694315b
permissions	-rw-r--r--