author | wenzelm |
Thu, 12 Apr 2007 15:01:13 +0200 | |
changeset 22648 | 8c6b4f7548e3 |
parent 19265 | cae36e16f3c0 |
child 23621 | e070a6ab1891 |
permissions | -rw-r--r-- |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Thy/latex.ML |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
4 |
|
15801 | 5 |
LaTeX presentation elements -- based on outer lexical syntax. |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
6 |
*) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
7 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
8 |
signature LATEX = |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
9 |
sig |
14924 | 10 |
val output_known_symbols: (string -> bool) * (string -> bool) -> |
11 |
Symbol.symbol list -> string |
|
11719 | 12 |
val output_symbols: Symbol.symbol list -> string |
17081 | 13 |
val output_basic: OuterLex.token -> string |
14 |
val output_markup: string -> string -> 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 |
|
9707 | 23 |
val tex_trailer: string |
9916 | 24 |
val isabelle_file: string -> string -> string |
14924 | 25 |
val symbol_source: (string -> bool) * (string -> bool) -> |
26 |
string -> Symbol.symbol list -> string |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
27 |
val theory_entry: string -> string |
9135 | 28 |
val modes: string list |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
29 |
end; |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
30 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
31 |
structure Latex: LATEX = |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
32 |
struct |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
33 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
34 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
35 |
(* symbol output *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
36 |
|
7900 | 37 |
local |
38 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
39 |
val output_chr = fn |
9505 | 40 |
" " => "\\ " | |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
41 |
"\n" => "\\isanewline\n" | |
9668 | 42 |
"!" => "{\\isacharbang}" | |
43 |
"\"" => "{\\isachardoublequote}" | |
|
9663 | 44 |
"#" => "{\\isacharhash}" | |
45 |
"$" => "{\\isachardollar}" | |
|
46 |
"%" => "{\\isacharpercent}" | |
|
47 |
"&" => "{\\isacharampersand}" | |
|
48 |
"'" => "{\\isacharprime}" | |
|
49 |
"(" => "{\\isacharparenleft}" | |
|
50 |
")" => "{\\isacharparenright}" | |
|
51 |
"*" => "{\\isacharasterisk}" | |
|
9668 | 52 |
"+" => "{\\isacharplus}" | |
53 |
"," => "{\\isacharcomma}" | |
|
9663 | 54 |
"-" => "{\\isacharminus}" | |
9668 | 55 |
"." => "{\\isachardot}" | |
56 |
"/" => "{\\isacharslash}" | |
|
57 |
":" => "{\\isacharcolon}" | |
|
58 |
";" => "{\\isacharsemicolon}" | |
|
9663 | 59 |
"<" => "{\\isacharless}" | |
9668 | 60 |
"=" => "{\\isacharequal}" | |
9663 | 61 |
">" => "{\\isachargreater}" | |
9668 | 62 |
"?" => "{\\isacharquery}" | |
63 |
"@" => "{\\isacharat}" | |
|
9663 | 64 |
"[" => "{\\isacharbrackleft}" | |
65 |
"\\" => "{\\isacharbackslash}" | |
|
66 |
"]" => "{\\isacharbrackright}" | |
|
67 |
"^" => "{\\isacharcircum}" | |
|
68 |
"_" => "{\\isacharunderscore}" | |
|
9668 | 69 |
"`" => "{\\isacharbackquote}" | |
9663 | 70 |
"{" => "{\\isacharbraceleft}" | |
71 |
"|" => "{\\isacharbar}" | |
|
72 |
"}" => "{\\isacharbraceright}" | |
|
73 |
"~" => "{\\isachartilde}" | |
|
14992 | 74 |
c => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
75 |
|
14924 | 76 |
val output_chrs = translate_string output_chr; |
77 |
||
78 |
fun output_known_sym (known_sym, known_ctrl) sym = |
|
14874 | 79 |
(case Symbol.decode sym of |
80 |
Symbol.Char s => output_chr s |
|
14924 | 81 |
| Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym |
82 |
| Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym |
|
14874 | 83 |
| Symbol.Raw s => s); |
7900 | 84 |
|
85 |
in |
|
86 |
||
14924 | 87 |
val output_known_symbols = implode oo (map o output_known_sym); |
88 |
val output_symbols = output_known_symbols (K true, K true); |
|
8192 | 89 |
val output_syms = output_symbols o Symbol.explode; |
7900 | 90 |
|
22648
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
91 |
val output_syms_antiqs = |
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
92 |
Antiquote.scan_antiquotes #> map |
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
93 |
(fn Antiquote.Text s => output_syms s |
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
94 |
| Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #> |
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
95 |
implode; |
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
96 |
|
7900 | 97 |
end; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
98 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
99 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
100 |
(* token output *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
101 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
102 |
structure T = OuterLex; |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
103 |
|
7756 | 104 |
val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment; |
105 |
||
17081 | 106 |
fun output_basic tok = |
107 |
let val s = T.val_of tok in |
|
108 |
if invisible_token tok then "" |
|
109 |
else if T.is_kind T.Command tok then |
|
110 |
"\\isacommand{" ^ output_syms s ^ "}" |
|
111 |
else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then |
|
112 |
"\\isakeyword{" ^ output_syms s ^ "}" |
|
17169 | 113 |
else if T.is_kind T.String tok then |
114 |
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) |
|
115 |
else if T.is_kind T.AltString tok then |
|
116 |
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) |
|
17186 | 117 |
else if T.is_kind T.Verbatim tok then |
22648
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
118 |
enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" |
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
119 |
(output_syms_antiqs (s, T.position_of tok)) |
17081 | 120 |
else output_syms s |
121 |
end; |
|
122 |
||
123 |
fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"; |
|
7745 | 124 |
|
17081 | 125 |
fun output_markup_env cmd txt = |
126 |
"%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ |
|
127 |
Symbol.strip_blanks txt ^ |
|
128 |
"%\n\\end{isamarkup" ^ cmd ^ "}%\n"; |
|
7756 | 129 |
|
17081 | 130 |
fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n"; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
131 |
|
17081 | 132 |
val markup_true = "\\isamarkuptrue%\n"; |
133 |
val markup_false = "\\isamarkupfalse%\n"; |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
134 |
|
17081 | 135 |
val begin_delim = enclose "%\n\\isadelim" "\n"; |
136 |
val end_delim = enclose "%\n\\endisadelim" "\n"; |
|
137 |
val begin_tag = enclose "%\n\\isatag" "\n"; |
|
138 |
fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg; |
|
11860 | 139 |
|
140 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
141 |
(* theory presentation *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
142 |
|
9707 | 143 |
val tex_trailer = |
144 |
"%%% Local Variables:\n\ |
|
9135 | 145 |
\%%% mode: latex\n\ |
146 |
\%%% TeX-master: \"root\"\n\ |
|
9144 | 147 |
\%%% End:\n"; |
8192 | 148 |
|
9916 | 149 |
fun isabelle_file name txt = |
150 |
"%\n\\begin{isabellebody}%\n\ |
|
10247 | 151 |
\\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ |
9916 | 152 |
"\\end{isabellebody}%\n" ^ tex_trailer; |
9707 | 153 |
|
14924 | 154 |
fun symbol_source known name syms = isabelle_file name |
155 |
("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^ |
|
156 |
output_known_symbols known syms); |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
157 |
|
9038
63d20536971f
session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents:
8965
diff
changeset
|
158 |
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n"; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
159 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
160 |
|
8460 | 161 |
(* print mode *) |
162 |
||
8965 | 163 |
val latexN = "latex"; |
17218 | 164 |
val modes = [latexN, Symbol.xsymbolsN]; |
8965 | 165 |
|
8460 | 166 |
fun latex_output str = |
167 |
let val syms = Symbol.explode str |
|
168 |
in (output_symbols syms, real (Symbol.length syms)) end; |
|
169 |
||
19265 | 170 |
fun latex_keyword cmd = |
171 |
apfst (enclose (if cmd then "\\isacommand{" else "\\isakeyword{") "}") o latex_output; |
|
172 |
||
10955 | 173 |
fun latex_indent "" = "" |
174 |
| latex_indent s = enclose "\\isaindent{" "}" s; |
|
175 |
||
19265 | 176 |
val _ = Output.add_mode latexN (latex_output, latex_keyword, latex_indent o #1, Symbol.encode_raw); |
8460 | 177 |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
178 |
end; |