isabelle-cookbook: CookBook/antiquote_setup_plus.ML@631d12c25bde (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
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	39	fun output_ml ml = output_verbatim
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
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	45	fun output_ml_response ml = output_verbatim
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	46	(fn ctxt => fn ((x as (rhs, pat), p), pos) =>
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	47	(ML_Context.eval_in (SOME ctxt) false pos (ml p x);
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	48	rhs ^ "\n" ^
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	49	space_implode "\n" (map (fn s => "> " ^ s)
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	50	(space_explode "\n" pat))));
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	51
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	52	fun output_ml_checked ml src ctxt (txt, pos) =
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	53	(ML_Context.eval_in (SOME ctxt) false pos (ml txt);
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	54	(if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	55	\|> (if ! ThyOutput.quotes then quote else I)
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	56	\|> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt)
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	57
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	58	fun check_file_exists ctxt name =
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	59	if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then ()
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	60	else error ("Source file " ^ quote name ^ " does not exist.")
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	61
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	62	val _ = ThyOutput.add_commands
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	63	[("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	64	(Scan.optional (Args.$$$ "for" \|-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	65	Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml ml_val_open)),
2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	66	("ML_response", ThyOutput.args (Scan.lift (OuterParse.position
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	67	((Args.name -- Args.name) >> rpair ()))) (output_ml_response (K ml_pat))),
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	68	("ML_file", ThyOutput.args (Scan.lift Args.name)
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	69	(ThyOutput.output (fn _ => fn name => (check_file_exists name; Pretty.str name)))),
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	70	("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	71	(ThyOutput.output (fn _ => fn s => Pretty.str s))),
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	72	("ML", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_val)),
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	73	("ML_struct", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_struct)),
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	74	("ML_type", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_type))];
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 26 diff changeset	75
26 2311f81d7a22 Added some more antiquotations. berghofe parents: 15 diff changeset	76	end;

author	Christian Urban <urbanc@in.tum.de>
	Fri, 17 Oct 2008 05:02:04 -0400
changeset 39	631d12c25bde
parent 26	2311f81d7a22
child 41	b11653b11bd3
permissions	-rw-r--r--