27 val add_keywords: string list -> unit |
27 val add_keywords: string list -> unit |
28 val inline_antiq: string -> |
28 val inline_antiq: string -> |
29 (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit |
29 (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit |
30 val value_antiq: string -> |
30 val value_antiq: string -> |
31 (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
31 (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
|
32 val proj_value_antiq: string -> (Context.generic * Args.T list -> |
|
33 (string * string * string) * (Context.generic * Args.T list)) -> unit |
32 val use_mltext: string -> bool -> Context.generic option -> unit |
34 val use_mltext: string -> bool -> Context.generic option -> unit |
33 val use_mltext_update: string -> bool -> Context.generic -> Context.generic |
35 val use_mltext_update: string -> bool -> Context.generic -> Context.generic |
34 val use_let: string -> string -> string -> Context.generic -> Context.generic |
36 val use_let: string -> string -> string -> Context.generic -> Context.generic |
35 val use: Path.T -> unit |
37 val use: Path.T -> unit |
36 end; |
38 end; |
81 change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)); |
83 change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)); |
82 |
84 |
83 |
85 |
84 (* maintain commands *) |
86 (* maintain commands *) |
85 |
87 |
86 datatype antiq = Inline of string | Value of string * string; |
88 datatype antiq = Inline of string | ProjValue of string * string * string; |
87 val global_parsers = ref (Symtab.empty: |
89 val global_parsers = ref (Symtab.empty: |
88 (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); |
90 (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); |
89 |
91 |
90 local |
92 local |
91 |
93 |
139 |
142 |
140 fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
143 fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
141 | expand (Antiquote.Antiq x) names = |
144 | expand (Antiquote.Antiq x) names = |
142 (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of |
145 (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of |
143 Inline s => (("", s), names) |
146 Inline s => (("", s), names) |
144 | Value (a, s) => |
147 | ProjValue (a, s, f) => |
145 let |
148 let |
146 val a' = if ML_Syntax.is_identifier a then a else "val"; |
149 val a' = if ML_Syntax.is_identifier a then a else "val"; |
147 val ([b], names') = Name.variants [a'] names; |
150 val ([b], names') = Name.variants [a'] names; |
148 in (("val " ^ b ^ " = " ^ s ^ ";\n", "Isabelle." ^ b), names') end); |
151 in (("val " ^ b ^ " = " ^ s ^ ";\n", f ^ " Isabelle." ^ b), names') end); |
149 |
152 |
150 val (decls, body) = |
153 val (decls, body) = |
151 fold_map expand ants ML_Syntax.reserved |
154 fold_map expand ants ML_Syntax.reserved |
152 |> #1 |> split_list |> pairself implode; |
155 |> #1 |> split_list |> pairself implode; |
153 in (isabelle_struct decls, body) end; |
156 in (isabelle_struct decls, body) end; |