isabelle-cookbook: CookBook/antiquote_setup_plus.ML@b11653b11bd3 (annotated)

15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	(*
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	Auxiliary antiquotations for the Cookbook.
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	3
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	*)
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	6	structure AntiquoteSetup: sig end =
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	7	struct
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	8
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	9	val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	10
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	11	fun ml_val ys txt = "fn " ^
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	12	(case ys of [] => "_" \| _ => enclose "(" ")" (commas ys)) ^
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	13	" => (" ^ txt ^ ");";
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	14
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	15	fun ml_val_open (ys, []) txt = ml_val ys txt
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	16	\| ml_val_open (ys, xs) txt =
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	17	ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	18
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	19	fun ml_pat (rhs, pat) =
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	20	let val pat' = implode (map (fn "\\<dots>" => "_" \| s => s)
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	21	(Symbol.explode pat))
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	22	in
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	23	"val " ^ pat' ^ " = " ^ rhs
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	24	end;
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	25
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	26	(* modified from original *)
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	27	fun ml_val txt = "fn _ => (" ^ txt ^ ");";
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	28	fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;";
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	29	fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	30
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	31	fun output_verbatim f src ctxt x =
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	32	let val txt = f ctxt x
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	33	in
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	34	(if ! ThyOutput.source then str_of_source src else txt)
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	35	\|> (if ! ThyOutput.quotes then quote else I)
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	36	\|> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	37	end;
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	38
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	39	fun output_ml_old ml = output_verbatim
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	40	(fn ctxt => fn ((txt, p), pos) =>
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	41	(ML_Context.eval_in (SOME ctxt) false pos (ml p txt);
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	42	txt \|> Source.of_string \|> ML_Lex.source \|> Source.exhaust \|>
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	43	Chunks.transform_cmts \|> implode));
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	44
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	45	fun output_ml ml src ctxt txt =
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	46	(ML_Context.eval_in (SOME ctxt) false Position.none (ml txt);
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	47	ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt)
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	48
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	49	fun add_response_indicator txt =
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	50	space_implode "\n" (map (fn s => "> " ^ s) (space_explode "\n" txt))
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	51
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	52	fun output_ml_response ml src ctxt (lhs,pat) =
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	53	(ML_Context.eval_in (SOME ctxt) false Position.none (ml (lhs,pat));
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	54	let val txt = lhs ^ "\n" ^ (add_response_indicator pat)
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	55	in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end)
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	56
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	57	fun output_ml_response_fake ml src ctxt (lhs,pat) =
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	58	(ML_Context.eval_in (SOME ctxt) false Position.none (ml lhs);
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	59	let val txt = lhs ^ "\n" ^ (add_response_indicator pat)
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	60	in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end)
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	61
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	62	fun check_file_exists ctxt name =
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	63	if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then ()
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	64	else error ("Source file " ^ quote name ^ " does not exist.")
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	65
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	66
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	67
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	68	val _ = ThyOutput.add_commands
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	69	[("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	70	(Scan.optional (Args.$$$ "for" \|-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	71	Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_old ml_val_open)),
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	72	("ML_file", ThyOutput.args (Scan.lift Args.name)
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	73	(ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))),
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	74	("ML_text", ThyOutput.args (Scan.lift Args.name)
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	75	(ThyOutput.output (fn _ => fn s => Pretty.str s))),
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	76	("ML", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val)),
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	77	("ML_response", ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response ml_pat)),
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	78	("ML_response_fake",
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	79	ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response_fake ml_val)),
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	80	("ML_struct", ThyOutput.args (Scan.lift Args.name) (output_ml ml_struct)),
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	81	("ML_type", ThyOutput.args (Scan.lift Args.name) (output_ml ml_type))];
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	82
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	83	end;

author	Christian Urban <urbanc@in.tum.de>
	Mon, 20 Oct 2008 06:22:11 +0000
changeset 41	b11653b11bd3
parent 39	631d12c25bde
child 42	cd612b489504
permissions	-rw-r--r--