author | wenzelm |
Tue, 06 Jun 2017 13:42:38 +0200 | |
changeset 66021 | 08ab52fb9db5 |
parent 66020 | a31760eee09d |
child 67145 | e77c5bfca9aa |
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 |
Author: Markus Wenzel, TU Muenchen |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
3 |
|
15801 | 4 |
LaTeX presentation elements -- based on outer lexical syntax. |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
5 |
*) |
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 |
signature LATEX = |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
8 |
sig |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
9 |
val output_ascii: string -> string |
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
10 |
val latex_control: Symbol.symbol |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
11 |
val is_latex_control: Symbol.symbol -> bool |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
12 |
val embed_raw: string -> string |
14924 | 13 |
val output_known_symbols: (string -> bool) * (string -> bool) -> |
14 |
Symbol.symbol list -> string |
|
11719 | 15 |
val output_symbols: Symbol.symbol list -> string |
61455 | 16 |
val output_token: Token.T -> string |
17081 | 17 |
val begin_delim: string -> string |
18 |
val end_delim: string -> string |
|
19 |
val begin_tag: string -> string |
|
20 |
val end_tag: string -> string |
|
61462 | 21 |
val environment: string -> string -> string |
9707 | 22 |
val tex_trailer: string |
58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset
|
23 |
val isabelle_theory: string -> string -> string |
14924 | 24 |
val symbol_source: (string -> bool) * (string -> bool) -> |
25 |
string -> Symbol.symbol list -> string |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
26 |
val theory_entry: string -> string |
66021 | 27 |
val latexN: string |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
28 |
end; |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
29 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
30 |
structure Latex: LATEX = |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
31 |
struct |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
32 |
|
61455 | 33 |
(* output verbatim ASCII *) |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
34 |
|
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
35 |
val output_ascii = |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
36 |
translate_string |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
37 |
(fn " " => "\\ " |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
38 |
| "\t" => "\\ " |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
39 |
| "\n" => "\\isanewline\n" |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
40 |
| s => |
61578 | 41 |
if exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
42 |
then enclose "{\\char`\\" "}" s else s); |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
43 |
|
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
44 |
|
61455 | 45 |
(* output symbols *) |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
46 |
|
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
47 |
val latex_control = "\<^latex>"; |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
48 |
fun is_latex_control s = s = latex_control; |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
49 |
|
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
50 |
val embed_raw = prefix latex_control o cartouche; |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
51 |
|
7900 | 52 |
local |
53 |
||
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
54 |
val char_table = |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
55 |
Symtab.make |
63590
4854f7ee0987
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents:
61595
diff
changeset
|
56 |
[("\007", "{\\isacharbell}"), |
4854f7ee0987
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents:
61595
diff
changeset
|
57 |
("!", "{\\isacharbang}"), |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
58 |
("\"", "{\\isachardoublequote}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
59 |
("#", "{\\isacharhash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
60 |
("$", "{\\isachardollar}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
61 |
("%", "{\\isacharpercent}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
62 |
("&", "{\\isacharampersand}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
63 |
("'", "{\\isacharprime}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
64 |
("(", "{\\isacharparenleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
65 |
(")", "{\\isacharparenright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
66 |
("*", "{\\isacharasterisk}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
67 |
("+", "{\\isacharplus}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
68 |
(",", "{\\isacharcomma}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
69 |
("-", "{\\isacharminus}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
70 |
(".", "{\\isachardot}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
71 |
("/", "{\\isacharslash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
72 |
(":", "{\\isacharcolon}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
73 |
(";", "{\\isacharsemicolon}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
74 |
("<", "{\\isacharless}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
75 |
("=", "{\\isacharequal}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
76 |
(">", "{\\isachargreater}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
77 |
("?", "{\\isacharquery}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
78 |
("@", "{\\isacharat}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
79 |
("[", "{\\isacharbrackleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
80 |
("\\", "{\\isacharbackslash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
81 |
("]", "{\\isacharbrackright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
82 |
("^", "{\\isacharcircum}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
83 |
("_", "{\\isacharunderscore}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
84 |
("`", "{\\isacharbackquote}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
85 |
("{", "{\\isacharbraceleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
86 |
("|", "{\\isacharbar}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
87 |
("}", "{\\isacharbraceright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
88 |
("~", "{\\isachartilde}")]; |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
89 |
|
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
90 |
fun output_chr " " = "\\ " |
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
43485
diff
changeset
|
91 |
| output_chr "\t" = "\\ " |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
92 |
| output_chr "\n" = "\\isanewline\n" |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
93 |
| output_chr c = |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
94 |
(case Symtab.lookup char_table c of |
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset
|
95 |
SOME s => s |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
96 |
| NONE => 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
|
97 |
|
14924 | 98 |
val output_chrs = translate_string output_chr; |
99 |
||
100 |
fun output_known_sym (known_sym, known_ctrl) sym = |
|
14874 | 101 |
(case Symbol.decode sym of |
102 |
Symbol.Char s => output_chr s |
|
37533
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36959
diff
changeset
|
103 |
| Symbol.UTF8 s => s |
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset
|
104 |
| Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym |
61475 | 105 |
| Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym |
43485 | 106 |
| Symbol.Malformed s => error (Symbol.malformed_msg s) |
107 |
| Symbol.EOF => error "Bad EOF symbol"); |
|
7900 | 108 |
|
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
109 |
val scan_latex_length = |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
110 |
Scan.many1 (fn (s, _) => Symbol.not_eof s andalso not (is_latex_control s)) |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
111 |
>> (Symbol.length o map Symbol_Pos.symbol) || |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
112 |
Scan.one (is_latex_control o Symbol_Pos.symbol) -- |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
113 |
Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0; |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
114 |
|
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
115 |
fun scan_latex known = |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
116 |
Scan.one (is_latex_control o Symbol_Pos.symbol) |-- |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
117 |
Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) || |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
118 |
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol); |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
119 |
|
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
120 |
fun read scan syms = |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
121 |
Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms); |
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
122 |
|
7900 | 123 |
in |
124 |
||
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
125 |
fun length_symbols syms = |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
126 |
fold Integer.add (these (read scan_latex_length syms)) 0; |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
127 |
|
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
128 |
fun output_known_symbols known syms = |
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
129 |
if exists is_latex_control syms then |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
130 |
(case read (scan_latex known) syms of |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
131 |
SOME ss => implode ss |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
132 |
| NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms))) |
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
133 |
else implode (map (output_known_sym known) syms); |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
134 |
|
14924 | 135 |
val output_symbols = output_known_symbols (K true, K true); |
8192 | 136 |
val output_syms = output_symbols o Symbol.explode; |
7900 | 137 |
|
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset
|
138 |
val output_syms_antiq = |
30589 | 139 |
(fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss) |
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
140 |
| Antiquote.Control {name = (name, _), body, ...} => |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
141 |
"\\isaantiqcontrol{" ^ output_symbols (Symbol.explode name) ^ "}" ^ |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
142 |
output_symbols (map Symbol_Pos.symbol body) |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
143 |
| Antiquote.Antiq {body, ...} => |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
144 |
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" |
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
145 |
(output_symbols (map Symbol_Pos.symbol body))); |
22648
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
146 |
|
7900 | 147 |
end; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
148 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
149 |
|
61455 | 150 |
(* output token *) |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
151 |
|
61455 | 152 |
fun output_token tok = |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset
|
153 |
let val s = Token.content_of tok in |
58861
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58727
diff
changeset
|
154 |
if Token.is_kind Token.Comment tok then "" |
46811
03a2dc9e0624
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents:
45666
diff
changeset
|
155 |
else if Token.is_command tok then |
17081 | 156 |
"\\isacommand{" ^ output_syms s ^ "}" |
50238
98d35a7368bd
more uniform Symbol.is_ascii_identifier in ML/Scala;
wenzelm
parents:
50201
diff
changeset
|
157 |
else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then |
17081 | 158 |
"\\isakeyword{" ^ output_syms s ^ "}" |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset
|
159 |
else if Token.is_kind Token.String tok then |
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset
|
160 |
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) |
59081 | 161 |
else if Token.is_kind Token.Alt_String tok then |
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset
|
162 |
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset
|
163 |
else if Token.is_kind Token.Verbatim tok then |
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset
|
164 |
let |
59809 | 165 |
val ants = Antiquote.read (Token.input_of tok); |
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset
|
166 |
val out = implode (map output_syms_antiq ants); |
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset
|
167 |
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end |
55033 | 168 |
else if Token.is_kind Token.Cartouche tok then |
169 |
enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s) |
|
17081 | 170 |
else output_syms s |
61404 | 171 |
end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); |
17081 | 172 |
|
61404 | 173 |
|
61455 | 174 |
(* tags *) |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
175 |
|
17081 | 176 |
val begin_delim = enclose "%\n\\isadelim" "\n"; |
177 |
val end_delim = enclose "%\n\\endisadelim" "\n"; |
|
178 |
val begin_tag = enclose "%\n\\isatag" "\n"; |
|
179 |
fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg; |
|
11860 | 180 |
|
181 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
182 |
(* theory presentation *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
183 |
|
61462 | 184 |
fun environment name = |
61516
8e3705d91cfa
clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
wenzelm
parents:
61505
diff
changeset
|
185 |
enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}"); |
61462 | 186 |
|
9707 | 187 |
val tex_trailer = |
188 |
"%%% Local Variables:\n\ |
|
9135 | 189 |
\%%% mode: latex\n\ |
190 |
\%%% TeX-master: \"root\"\n\ |
|
9144 | 191 |
\%%% End:\n"; |
8192 | 192 |
|
58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset
|
193 |
fun isabelle_theory name txt = |
9916 | 194 |
"%\n\\begin{isabellebody}%\n\ |
58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset
|
195 |
\\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ |
61462 | 196 |
"%\n\\end{isabellebody}%\n" ^ tex_trailer; |
9707 | 197 |
|
58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset
|
198 |
fun symbol_source known name syms = |
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset
|
199 |
isabelle_theory name |
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset
|
200 |
("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^ |
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset
|
201 |
output_known_symbols known syms); |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
202 |
|
9038
63d20536971f
session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents:
8965
diff
changeset
|
203 |
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n"; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
204 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
205 |
|
8460 | 206 |
(* print mode *) |
207 |
||
8965 | 208 |
val latexN = "latex"; |
209 |
||
8460 | 210 |
fun latex_output str = |
211 |
let val syms = Symbol.explode str |
|
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
212 |
in (output_symbols syms, length_symbols syms) end; |
19265 | 213 |
|
23621 | 214 |
fun latex_markup (s, _) = |
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset
|
215 |
if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N |
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset
|
216 |
then ("\\isacommand{", "}") |
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset
|
217 |
else if s = Markup.keyword2N |
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset
|
218 |
then ("\\isakeyword{", "}") |
29325 | 219 |
else Markup.no_output; |
10955 | 220 |
|
23621 | 221 |
fun latex_indent "" _ = "" |
222 |
| latex_indent s _ = enclose "\\isaindent{" "}" s; |
|
223 |
||
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
224 |
val _ = Output.add_mode latexN latex_output embed_raw; |
23703 | 225 |
val _ = Markup.add_mode latexN latex_markup; |
226 |
val _ = Pretty.add_mode latexN latex_indent; |
|
8460 | 227 |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
228 |
end; |