4 Miscellaneous ML antiquotations. |
4 Miscellaneous ML antiquotations. |
5 *) |
5 *) |
6 |
6 |
7 structure ML_Antiquotations: sig end = |
7 structure ML_Antiquotations: sig end = |
8 struct |
8 struct |
|
9 |
|
10 (* ML support *) |
|
11 |
|
12 val _ = Theory.setup |
|
13 (ML_Antiquotation.inline @{binding assert} |
|
14 (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> |
|
15 |
|
16 ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #> |
|
17 |
|
18 ML_Antiquotation.declaration @{binding print} |
|
19 (Scan.lift (Scan.optional Args.name "Output.writeln")) |
|
20 (fn src => fn output => fn ctxt => |
|
21 let |
|
22 val (_, pos) = Token.name_of_src src; |
|
23 val (a, ctxt') = ML_Antiquotation.variant "output" ctxt; |
|
24 val env = |
|
25 "val " ^ a ^ ": string -> unit =\n\ |
|
26 \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ |
|
27 ML_Syntax.print_position pos ^ "));\n"; |
|
28 val body = |
|
29 "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))"; |
|
30 in (K (env, body), ctxt') end)); |
|
31 |
|
32 |
|
33 (* embedded source *) |
|
34 |
|
35 val _ = Theory.setup |
|
36 (ML_Antiquotation.value @{binding source} |
|
37 (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} => |
|
38 "{delimited = " ^ Bool.toString delimited ^ |
|
39 ", text = " ^ ML_Syntax.print_string text ^ |
|
40 ", pos = " ^ ML_Syntax.print_position pos ^ "}"))); |
|
41 |
|
42 |
|
43 (* formal entities *) |
9 |
44 |
10 val _ = Theory.setup |
45 val _ = Theory.setup |
11 (ML_Antiquotation.value @{binding system_option} |
46 (ML_Antiquotation.value @{binding system_option} |
12 (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => |
47 (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => |
13 (Context_Position.report ctxt pos (Options.default_markup (name, pos)); |
48 (Context_Position.report ctxt pos (Options.default_markup (name, pos)); |
48 ML_Antiquotation.value @{binding cpat} |
83 ML_Antiquotation.value @{binding cpat} |
49 (Args.context -- |
84 (Args.context -- |
50 Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t => |
85 Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t => |
51 "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ |
86 "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ |
52 ML_Syntax.atomic (ML_Syntax.print_term t)))); |
87 ML_Syntax.atomic (ML_Syntax.print_term t)))); |
53 |
|
54 |
|
55 (* embedded source *) |
|
56 |
|
57 val _ = Theory.setup |
|
58 (ML_Antiquotation.value @{binding source} |
|
59 (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} => |
|
60 "{delimited = " ^ Bool.toString delimited ^ |
|
61 ", text = " ^ ML_Syntax.print_string text ^ |
|
62 ", pos = " ^ ML_Syntax.print_position pos ^ "}"))); |
|
63 |
|
64 |
|
65 (* ML support *) |
|
66 |
|
67 val _ = Theory.setup |
|
68 (ML_Antiquotation.inline @{binding assert} |
|
69 (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> |
|
70 |
|
71 ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #> |
|
72 |
|
73 ML_Antiquotation.declaration @{binding print} |
|
74 (Scan.lift (Scan.optional Args.name "Output.writeln")) |
|
75 (fn src => fn output => fn ctxt => |
|
76 let |
|
77 val (_, pos) = Token.name_of_src src; |
|
78 val (a, ctxt') = ML_Antiquotation.variant "output" ctxt; |
|
79 val env = |
|
80 "val " ^ a ^ ": string -> unit =\n\ |
|
81 \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ |
|
82 ML_Syntax.print_position pos ^ "));\n"; |
|
83 val body = |
|
84 "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))"; |
|
85 in (K (env, body), ctxt') end)); |
|
86 |
88 |
87 |
89 |
88 (* type classes *) |
90 (* type classes *) |
89 |
91 |
90 fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => |
92 fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => |