8 signature LATEX = |
8 signature LATEX = |
9 sig |
9 sig |
10 val output_known_symbols: (string -> bool) * (string -> bool) -> |
10 val output_known_symbols: (string -> bool) * (string -> bool) -> |
11 Symbol.symbol list -> string |
11 Symbol.symbol list -> string |
12 val output_symbols: Symbol.symbol list -> string |
12 val output_symbols: Symbol.symbol list -> string |
13 datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim |
13 val output_basic: OuterLex.token -> string |
14 val output_tokens: (token * string) list -> string |
14 val output_markup: string -> string -> string |
15 val flag_markup: bool -> string |
15 val output_markup_env: string -> string -> string |
|
16 val output_verbatim: string -> string |
|
17 val markup_true: string |
|
18 val markup_false: string |
|
19 val begin_delim: string -> string |
|
20 val end_delim: string -> string |
|
21 val begin_tag: string -> string |
|
22 val end_tag: string -> string |
16 val tex_trailer: string |
23 val tex_trailer: string |
17 val isabelle_file: string -> string -> string |
24 val isabelle_file: string -> string -> string |
18 val symbol_source: (string -> bool) * (string -> bool) -> |
25 val symbol_source: (string -> bool) * (string -> bool) -> |
19 string -> Symbol.symbol list -> string |
26 string -> Symbol.symbol list -> string |
20 val theory_entry: string -> string |
27 val theory_entry: string -> string |
86 |
93 |
87 (* token output *) |
94 (* token output *) |
88 |
95 |
89 structure T = OuterLex; |
96 structure T = OuterLex; |
90 |
97 |
91 datatype token = |
|
92 Basic of T.token | |
|
93 Markup of string | |
|
94 MarkupEnv of string | |
|
95 Verbatim; |
|
96 |
|
97 |
|
98 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment; |
98 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment; |
99 |
99 |
100 fun output_tok (Basic tok, _) = |
100 fun output_basic tok = |
101 let val s = T.val_of tok in |
101 let val s = T.val_of tok in |
102 if invisible_token tok then "" |
102 if invisible_token tok then "" |
103 else if T.is_kind T.Command tok then |
103 else if T.is_kind T.Command tok then |
104 "\\isacommand{" ^ output_syms s ^ "}" |
104 "\\isacommand{" ^ output_syms s ^ "}" |
105 else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then |
105 else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then |
106 "\\isakeyword{" ^ output_syms s ^ "}" |
106 "\\isakeyword{" ^ output_syms s ^ "}" |
107 else if T.is_kind T.String tok then output_syms (Library.quote s) |
107 else if T.is_kind T.String tok then output_syms (Library.quote s) |
108 else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s) |
108 else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s) |
109 else output_syms s |
109 else output_syms s |
110 end |
110 end; |
111 | output_tok (Markup cmd, txt) = |
|
112 "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n" |
|
113 | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ |
|
114 Symbol.strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n" |
|
115 | output_tok (Verbatim, txt) = "%\n" ^ Symbol.strip_blanks txt ^ "\n"; |
|
116 |
111 |
|
112 fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"; |
117 |
113 |
118 val output_tokens = implode o map output_tok; |
114 fun output_markup_env cmd txt = |
|
115 "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ |
|
116 Symbol.strip_blanks txt ^ |
|
117 "%\n\\end{isamarkup" ^ cmd ^ "}%\n"; |
119 |
118 |
|
119 fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n"; |
120 |
120 |
121 fun flag_markup true = "\\isamarkuptrue%\n" |
121 val markup_true = "\\isamarkuptrue%\n"; |
122 | flag_markup false = "\\isamarkupfalse%\n"; |
122 val markup_false = "\\isamarkupfalse%\n"; |
|
123 |
|
124 val begin_delim = enclose "%\n\\isadelim" "\n"; |
|
125 val end_delim = enclose "%\n\\endisadelim" "\n"; |
|
126 val begin_tag = enclose "%\n\\isatag" "\n"; |
|
127 fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg; |
123 |
128 |
124 |
129 |
125 (* theory presentation *) |
130 (* theory presentation *) |
126 |
131 |
127 val tex_trailer = |
132 val tex_trailer = |