equal
deleted
inserted
replaced
8 signature SYNTAX = |
8 signature SYNTAX = |
9 sig |
9 sig |
10 type operations |
10 type operations |
11 val install_operations: operations -> theory -> theory |
11 val install_operations: operations -> theory -> theory |
12 val root: string Config.T |
12 val root: string Config.T |
13 val ambiguity_warning_raw: Config.raw |
|
14 val ambiguity_warning: bool Config.T |
13 val ambiguity_warning: bool Config.T |
15 val ambiguity_limit_raw: Config.raw |
|
16 val ambiguity_limit: int Config.T |
14 val ambiguity_limit: int Config.T |
17 val encode_input: Input.source -> XML.tree |
15 val encode_input: Input.source -> XML.tree |
18 val implode_input: Input.source -> string |
16 val implode_input: Input.source -> string |
19 val read_input_pos: string -> Position.T |
17 val read_input_pos: string -> Position.T |
20 val read_input: string -> Input.source |
18 val read_input: string -> Input.source |
159 | SOME ops => which ops ctxt x); |
157 | SOME ops => which ops ctxt x); |
160 |
158 |
161 |
159 |
162 (* configuration options *) |
160 (* configuration options *) |
163 |
161 |
164 val root = Config.string (Config.declare ("syntax_root", \<^here>) (K (Config.String "any"))); |
162 val root = Config.declare_string ("syntax_root", \<^here>) (K "any"); |
165 |
163 val ambiguity_warning = Config.declare_bool ("syntax_ambiguity_warning", \<^here>) (K true); |
166 val ambiguity_warning_raw = |
164 val ambiguity_limit = Config.declare_int ("syntax_ambiguity_limit", \<^here>) (K 10); |
167 Config.declare ("syntax_ambiguity_warning", \<^here>) (fn _ => Config.Bool true); |
|
168 val ambiguity_warning = Config.bool ambiguity_warning_raw; |
|
169 |
|
170 val ambiguity_limit_raw = |
|
171 Config.declare ("syntax_ambiguity_limit", \<^here>) (fn _ => Config.Int 10); |
|
172 val ambiguity_limit = Config.int ambiguity_limit_raw; |
|
173 |
165 |
174 |
166 |
175 (* formal input *) |
167 (* formal input *) |
176 |
168 |
177 fun encode_input source = |
169 fun encode_input source = |
328 val string_of_arity = Pretty.string_of oo pretty_arity; |
320 val string_of_arity = Pretty.string_of oo pretty_arity; |
329 |
321 |
330 |
322 |
331 (* global pretty printing *) |
323 (* global pretty printing *) |
332 |
324 |
333 val pretty_global = |
325 val pretty_global = Config.declare_bool ("Syntax.pretty_global", \<^here>) (K false); |
334 Config.bool (Config.declare ("Syntax.pretty_global", \<^here>) (K (Config.Bool false))); |
|
335 fun is_pretty_global ctxt = Config.get ctxt pretty_global; |
326 fun is_pretty_global ctxt = Config.get ctxt pretty_global; |
336 val set_pretty_global = Config.put pretty_global; |
327 val set_pretty_global = Config.put pretty_global; |
337 val init_pretty_global = set_pretty_global true o Proof_Context.init_global; |
328 val init_pretty_global = set_pretty_global true o Proof_Context.init_global; |
338 val init_pretty = Context.cases init_pretty_global I; |
329 val init_pretty = Context.cases init_pretty_global I; |
339 |
330 |