9 val display: bool Unsynchronized.ref |
9 val display: bool Unsynchronized.ref |
10 val quotes: bool Unsynchronized.ref |
10 val quotes: bool Unsynchronized.ref |
11 val indent: int Unsynchronized.ref |
11 val indent: int Unsynchronized.ref |
12 val source: bool Unsynchronized.ref |
12 val source: bool Unsynchronized.ref |
13 val break: bool Unsynchronized.ref |
13 val break: bool Unsynchronized.ref |
14 val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit |
14 val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context |
15 val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit |
15 val add_option: string -> (string -> Proof.context -> Proof.context) -> unit |
16 val defined_command: string -> bool |
16 val defined_command: string -> bool |
17 val defined_option: string -> bool |
17 val defined_option: string -> bool |
18 val print_antiquotations: unit -> unit |
18 val print_antiquotations: unit -> unit |
19 val boolean: string -> bool |
19 val boolean: string -> bool |
20 val integer: string -> int |
20 val integer: string -> int |
21 val antiquotation: string -> 'a context_parser -> |
21 val antiquotation: string -> 'a context_parser -> |
22 ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit |
22 ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit |
23 datatype markup = Markup | MarkupEnv | Verbatim |
23 datatype markup = Markup | MarkupEnv | Verbatim |
24 val modes: string list Unsynchronized.ref |
24 val modes: string list Unsynchronized.ref |
25 val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string |
25 val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string |
26 val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) -> |
26 val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) -> |
27 (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T |
27 (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T |
43 val indent = Unsynchronized.ref 0; |
43 val indent = Unsynchronized.ref 0; |
44 val source = Unsynchronized.ref false; |
44 val source = Unsynchronized.ref false; |
45 val break = Unsynchronized.ref false; |
45 val break = Unsynchronized.ref false; |
46 |
46 |
47 |
47 |
|
48 structure Wrappers = Proof_Data |
|
49 ( |
|
50 type T = ((unit -> string) -> unit -> string) list; |
|
51 fun init _ = []; |
|
52 ); |
|
53 |
|
54 fun add_wrapper wrapper = Wrappers.map (cons wrapper); |
|
55 |
|
56 val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f); |
|
57 |
|
58 |
48 |
59 |
49 (** maintain global antiquotations **) |
60 (** maintain global antiquotations **) |
50 |
61 |
51 local |
62 local |
52 |
63 |
53 val global_commands = |
64 val global_commands = |
54 Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table); |
65 Unsynchronized.ref |
|
66 (Symtab.empty: (Args.src -> Toplevel.state -> Proof.context -> string) Symtab.table); |
55 |
67 |
56 val global_options = |
68 val global_options = |
57 Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table); |
69 Unsynchronized.ref (Symtab.empty: (string -> Proof.context -> Proof.context) Symtab.table); |
58 |
70 |
59 fun add_item kind (name, x) tab = |
71 fun add_item kind name item tab = |
60 (if not (Symtab.defined tab name) then () |
72 (if not (Symtab.defined tab name) then () |
61 else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name); |
73 else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name); |
62 Symtab.update (name, x) tab); |
74 Symtab.update (name, item) tab); |
63 |
75 |
64 in |
76 in |
65 |
77 |
66 fun add_commands xs = |
78 fun add_command name cmd = |
67 CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs)); |
79 CRITICAL (fn () => Unsynchronized.change global_commands (add_item "command" name cmd)); |
68 fun add_options xs = |
80 fun add_option name opt = |
69 CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs)); |
81 CRITICAL (fn () => Unsynchronized.change global_options (add_item "option" name opt)); |
70 |
82 |
71 fun defined_command name = Symtab.defined (! global_commands) name; |
83 fun defined_command name = Symtab.defined (! global_commands) name; |
72 fun defined_option name = Symtab.defined (! global_options) name; |
84 fun defined_option name = Symtab.defined (! global_options) name; |
73 |
85 |
74 fun command src = |
86 fun command src = |
75 let val ((name, _), pos) = Args.dest_src src in |
87 let val ((name, _), pos) = Args.dest_src src in |
76 (case Symtab.lookup (! global_commands) name of |
88 (case Symtab.lookup (! global_commands) name of |
77 NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos) |
89 NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos) |
78 | SOME f => |
90 | SOME f => |
79 (Position.report (Markup.doc_antiq name) pos; |
91 (Position.report (Markup.doc_antiq name) pos; |
80 (fn state => f src state handle ERROR msg => |
92 (fn state => fn ctxt => f src state ctxt handle ERROR msg => |
81 cat_error msg ("The error(s) above occurred in document antiquotation: " ^ |
93 cat_error msg ("The error(s) above occurred in document antiquotation: " ^ |
82 quote name ^ Position.str_of pos)))) |
94 quote name ^ Position.str_of pos)))) |
83 end; |
95 end; |
84 |
96 |
85 fun option (name, s) f () = |
97 fun option (name, s) ctxt = |
86 (case Symtab.lookup (! global_options) name of |
98 (case Symtab.lookup (! global_options) name of |
87 NONE => error ("Unknown document antiquotation option: " ^ quote name) |
99 NONE => error ("Unknown document antiquotation option: " ^ quote name) |
88 | SOME opt => opt s f ()); |
100 | SOME opt => opt s ctxt); |
89 |
|
90 fun options [] f = f |
|
91 | options (opt :: opts) f = option opt (options opts f); |
|
92 |
101 |
93 |
102 |
94 fun print_antiquotations () = |
103 fun print_antiquotations () = |
95 [Pretty.big_list "document antiquotation commands:" |
104 [Pretty.big_list "document antiquotation commands:" |
96 (map Pretty.str (sort_strings (Symtab.keys (! global_commands)))), |
105 (map Pretty.str (sort_strings (Symtab.keys (! global_commands)))), |
98 (map Pretty.str (sort_strings (Symtab.keys (! global_options))))] |
107 (map Pretty.str (sort_strings (Symtab.keys (! global_options))))] |
99 |> Pretty.chunks |> Pretty.writeln; |
108 |> Pretty.chunks |> Pretty.writeln; |
100 |
109 |
101 end; |
110 end; |
102 |
111 |
103 fun antiquotation name scan out = add_commands [(name, fn src => fn state => |
112 fun antiquotation name scan out = |
104 let val (x, ctxt) = Args.context_syntax "document antiquotation" |
113 add_command name |
105 scan src (Toplevel.presentation_context_of state) |
114 (fn src => fn state => fn ctxt => |
106 in out {source = src, state = state, context = ctxt} x end)]; |
115 let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt |
|
116 in out {source = src, state = state, context = ctxt'} x end); |
107 |
117 |
108 |
118 |
109 |
119 |
110 (** syntax of antiquotations **) |
120 (** syntax of antiquotations **) |
111 |
121 |
149 |
159 |
150 fun eval_antiquote lex state (txt, pos) = |
160 fun eval_antiquote lex state (txt, pos) = |
151 let |
161 let |
152 fun expand (Antiquote.Text ss) = Symbol_Pos.content ss |
162 fun expand (Antiquote.Text ss) = Symbol_Pos.content ss |
153 | expand (Antiquote.Antiq (ss, (pos, _))) = |
163 | expand (Antiquote.Antiq (ss, (pos, _))) = |
154 let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in |
164 let |
155 options opts (fn () => command src state) (); (*preview errors!*) |
165 val (opts, src) = Token.read_antiq lex antiq (ss, pos); |
156 Print_Mode.with_modes (! modes @ Latex.modes) |
166 val opts_ctxt = fold option opts (Toplevel.presentation_context_of state); |
157 (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) () |
167 val cmd = wrap opts_ctxt (fn () => command src state opts_ctxt); |
|
168 val _ = cmd (); (*preview errors!*) |
|
169 in |
|
170 Print_Mode.with_modes (! modes @ Latex.modes) (Output.no_warnings_CRITICAL cmd) () |
158 end |
171 end |
159 | expand (Antiquote.Open _) = "" |
172 | expand (Antiquote.Open _) = "" |
160 | expand (Antiquote.Close _) = ""; |
173 | expand (Antiquote.Close _) = ""; |
161 val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); |
174 val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); |
162 in |
175 in |
415 |
428 |
416 (** setup default output **) |
429 (** setup default output **) |
417 |
430 |
418 (* options *) |
431 (* options *) |
419 |
432 |
420 val _ = add_options |
433 val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean); |
421 [("show_types", setmp_CRITICAL Syntax.show_types o boolean), |
434 val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean); |
422 ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean), |
435 val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean); |
423 ("show_structs", setmp_CRITICAL show_structs o boolean), |
436 val _ = add_option "show_question_marks" (add_wrapper o setmp_CRITICAL show_question_marks o boolean); |
424 ("show_question_marks", setmp_CRITICAL show_question_marks o boolean), |
437 val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean); |
425 ("long_names", setmp_CRITICAL Name_Space.long_names o boolean), |
438 val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean); |
426 ("short_names", setmp_CRITICAL Name_Space.short_names o boolean), |
439 val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean); |
427 ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean), |
440 val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean); |
428 ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean), |
441 val _ = add_option "display" (add_wrapper o setmp_CRITICAL display o boolean); |
429 ("display", setmp_CRITICAL display o boolean), |
442 val _ = add_option "break" (add_wrapper o setmp_CRITICAL break o boolean); |
430 ("break", setmp_CRITICAL break o boolean), |
443 val _ = add_option "quotes" (add_wrapper o setmp_CRITICAL quotes o boolean); |
431 ("quotes", setmp_CRITICAL quotes o boolean), |
444 val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single); |
432 ("mode", fn s => fn f => Print_Mode.with_modes [s] f), |
445 val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer); |
433 ("margin", setmp_CRITICAL Pretty.margin_default o integer), |
446 val _ = add_option "indent" (add_wrapper o setmp_CRITICAL indent o integer); |
434 ("indent", setmp_CRITICAL indent o integer), |
447 val _ = add_option "source" (add_wrapper o setmp_CRITICAL source o boolean); |
435 ("source", setmp_CRITICAL source o boolean), |
448 val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer); |
436 ("goals_limit", setmp_CRITICAL goals_limit o integer)]; |
|
437 |
449 |
438 |
450 |
439 (* basic pretty printing *) |
451 (* basic pretty printing *) |
440 |
452 |
441 fun tweak_line s = |
453 fun tweak_line s = |