44 | Symbol.Control s => "\\092<^" ^ s ^ ">" |
40 | Symbol.Control s => "\\092<^" ^ s ^ ">" |
45 | _ => translate_string (print_codepoint o ord) sym); |
41 | _ => translate_string (print_codepoint o ord) sym); |
46 |
42 |
47 val print_string = quote o implode o map print_symbol o Symbol.explode; |
43 val print_string = quote o implode o map print_symbol o Symbol.explode; |
48 |
44 |
49 |
|
50 (** antiquotations **) |
|
51 |
|
52 (* theory data *) |
|
53 |
|
54 structure Antiqs = Theory_Data |
|
55 ( |
|
56 type T = (Token.src -> Proof.context -> string) Name_Space.table; |
|
57 val empty : T = Name_Space.empty_table Markup.haskell_antiquotationN; |
|
58 val extend = I; |
|
59 fun merge tabs : T = Name_Space.merge_tables tabs; |
|
60 ); |
|
61 |
|
62 val get_antiquotations = Antiqs.get o Proof_Context.theory_of; |
|
63 |
|
64 fun antiquotation name scan body thy = |
|
65 let |
|
66 fun antiq src ctxt = |
|
67 let val (x, ctxt') = Token.syntax scan src ctxt |
|
68 in body {context = ctxt', source = src, argument = x} end; |
|
69 in thy |> Antiqs.map (Name_Space.define (Context.Theory thy) true (name, antiq) #> #2) end; |
|
70 |
|
71 |
|
72 (* read source and expand antiquotations *) |
|
73 |
|
74 val scan_antiq = |
|
75 Antiquote.scan_control >> Antiquote.Control || |
|
76 Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol); |
|
77 |
|
78 fun read_source ctxt source = |
|
79 let |
|
80 val _ = |
|
81 Context_Position.report ctxt (Input.pos_of source) |
|
82 (Markup.language_haskell (Input.is_delimited source)); |
|
83 |
|
84 val (input, _) = |
|
85 Input.source_explode source |
|
86 |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq)); |
|
87 |
|
88 val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input); |
|
89 |
|
90 fun expand antiq = |
|
91 (case antiq of |
|
92 Antiquote.Text s => s |
|
93 | Antiquote.Control {name, body, ...} => |
|
94 let |
|
95 val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]); |
|
96 val (src', f) = Token.check_src ctxt get_antiquotations src; |
|
97 in f src' ctxt end |
|
98 | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq)))); |
|
99 in implode (map expand input) end; |
|
100 |
|
101 |
|
102 (* concrete antiquotation: ML expression as Haskell string literal *) |
|
103 |
|
104 structure Local_Data = Proof_Data |
|
105 ( |
|
106 type T = string option; |
|
107 fun init _ = NONE; |
|
108 ); |
|
109 |
|
110 val set_result = Local_Data.put o SOME; |
|
111 |
|
112 fun the_result ctxt = |
|
113 (case Local_Data.get ctxt of |
|
114 SOME s => s |
|
115 | NONE => raise Fail "No result"); |
|
116 |
|
117 fun path_antiq check = |
|
118 Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => |
|
119 (check ctxt Path.current (name, pos) |> Path.implode |> print_string)); |
|
120 |
|
121 val _ = |
|
122 Theory.setup |
|
123 (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input) |
|
124 (fn {context = ctxt, argument, ...} => |
|
125 ctxt |> Context.proof_map |
|
126 (ML_Context.expression (Input.pos_of argument) |
|
127 (ML_Lex.read "Theory.local_setup (GHC.set_result (" @ |
|
128 ML_Lex.read_source argument @ ML_Lex.read "))")) |
|
129 |> the_result |> print_string) #> |
|
130 antiquotation \<^binding>\<open>path\<close> (path_antiq Resources.check_path) #argument #> |
|
131 antiquotation \<^binding>\<open>file\<close> (path_antiq Resources.check_file) #argument #> |
|
132 antiquotation \<^binding>\<open>dir\<close> (path_antiq Resources.check_dir) #argument); |
|
133 |
|
134 end; |
45 end; |