author | Christian Sternagel |
Thu, 30 Aug 2012 13:03:03 +0900 | |
changeset 49086 | 835fd053d17d |
parent 48628 | 4dd1d4585902 |
child 49320 | 94bd2fb83d11 |
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 |
14924 | 9 |
val output_known_symbols: (string -> bool) * (string -> bool) -> |
10 |
Symbol.symbol list -> string |
|
11719 | 11 |
val output_symbols: Symbol.symbol list -> string |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset
|
12 |
val output_basic: Token.T -> string |
17081 | 13 |
val output_markup: string -> string -> string |
14 |
val output_markup_env: string -> string -> string |
|
15 |
val output_verbatim: string -> string |
|
16 |
val markup_true: string |
|
17 |
val markup_false: string |
|
18 |
val begin_delim: string -> string |
|
19 |
val end_delim: string -> string |
|
20 |
val begin_tag: string -> string |
|
21 |
val end_tag: string -> string |
|
9707 | 22 |
val tex_trailer: string |
9916 | 23 |
val isabelle_file: 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 |
9135 | 27 |
val modes: string list |
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 |
|
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
33 |
(* literal text *) |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
34 |
|
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
35 |
local |
48628
4dd1d4585902
more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;
wenzelm
parents:
46811
diff
changeset
|
36 |
fun hex_nibble i = |
4dd1d4585902
more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;
wenzelm
parents:
46811
diff
changeset
|
37 |
if i < 10 then string_of_int i |
4dd1d4585902
more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;
wenzelm
parents:
46811
diff
changeset
|
38 |
else chr (ord "A" + i - 10); |
4dd1d4585902
more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;
wenzelm
parents:
46811
diff
changeset
|
39 |
|
4dd1d4585902
more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;
wenzelm
parents:
46811
diff
changeset
|
40 |
fun hex_byte c = hex_nibble (ord c div 16) ^ hex_nibble (ord c mod 16); |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
41 |
in |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
42 |
|
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
43 |
fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}"; |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
44 |
fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg); |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
45 |
|
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
46 |
end; |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
47 |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
48 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
49 |
(* symbol output *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
50 |
|
7900 | 51 |
local |
52 |
||
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
53 |
val char_table = |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
54 |
Symtab.make |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
55 |
[("!", "{\\isacharbang}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
56 |
("\"", "{\\isachardoublequote}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
57 |
("#", "{\\isacharhash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
58 |
("$", "{\\isachardollar}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
59 |
("%", "{\\isacharpercent}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
60 |
("&", "{\\isacharampersand}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
61 |
("'", "{\\isacharprime}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
62 |
("(", "{\\isacharparenleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
63 |
(")", "{\\isacharparenright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
64 |
("*", "{\\isacharasterisk}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
65 |
("+", "{\\isacharplus}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
66 |
(",", "{\\isacharcomma}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
67 |
("-", "{\\isacharminus}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
68 |
(".", "{\\isachardot}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
69 |
("/", "{\\isacharslash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
70 |
(":", "{\\isacharcolon}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
71 |
(";", "{\\isacharsemicolon}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
72 |
("<", "{\\isacharless}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
73 |
("=", "{\\isacharequal}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
74 |
(">", "{\\isachargreater}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
75 |
("?", "{\\isacharquery}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
76 |
("@", "{\\isacharat}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
77 |
("[", "{\\isacharbrackleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
78 |
("\\", "{\\isacharbackslash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
79 |
("]", "{\\isacharbrackright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
80 |
("^", "{\\isacharcircum}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
81 |
("_", "{\\isacharunderscore}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
82 |
("`", "{\\isacharbackquote}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
83 |
("{", "{\\isacharbraceleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
84 |
("|", "{\\isacharbar}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
85 |
("}", "{\\isacharbraceright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
86 |
("~", "{\\isachartilde}")]; |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
87 |
|
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
88 |
fun output_chr " " = "\\ " |
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
43485
diff
changeset
|
89 |
| 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
|
90 |
| 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
|
91 |
| output_chr c = |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
92 |
(case Symtab.lookup char_table c of |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
93 |
SOME s => enclose_literal c s |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
94 |
| 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
|
95 |
|
14924 | 96 |
val output_chrs = translate_string output_chr; |
97 |
||
98 |
fun output_known_sym (known_sym, known_ctrl) sym = |
|
14874 | 99 |
(case Symbol.decode sym of |
100 |
Symbol.Char s => output_chr s |
|
37533
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36959
diff
changeset
|
101 |
| Symbol.UTF8 s => s |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
102 |
| Symbol.Sym s => |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
103 |
if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s) |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
104 |
else output_chrs sym |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
105 |
| Symbol.Ctrl s => |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
106 |
if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
107 |
else output_chrs sym |
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40402
diff
changeset
|
108 |
| Symbol.Raw s => s |
43485 | 109 |
| Symbol.Malformed s => error (Symbol.malformed_msg s) |
110 |
| Symbol.EOF => error "Bad EOF symbol"); |
|
7900 | 111 |
|
112 |
in |
|
113 |
||
14924 | 114 |
val output_known_symbols = implode oo (map o output_known_sym); |
115 |
val output_symbols = output_known_symbols (K true, K true); |
|
8192 | 116 |
val output_syms = output_symbols o Symbol.explode; |
7900 | 117 |
|
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset
|
118 |
val output_syms_antiq = |
30589 | 119 |
(fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss) |
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset
|
120 |
| Antiquote.Antiq (ss, _) => |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
121 |
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
122 |
(output_symbols (map Symbol_Pos.symbol ss)) |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
123 |
| Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}" |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
124 |
| Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}"); |
22648
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset
|
125 |
|
7900 | 126 |
end; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
127 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
128 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
129 |
(* token output *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
130 |
|
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset
|
131 |
val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment; |
7756 | 132 |
|
17081 | 133 |
fun output_basic 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
|
134 |
let val s = Token.content_of tok in |
17081 | 135 |
if invisible_token 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
|
136 |
else if Token.is_command tok then |
17081 | 137 |
"\\isacommand{" ^ output_syms s ^ "}" |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40523
diff
changeset
|
138 |
else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then |
17081 | 139 |
"\\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
|
140 |
else if Token.is_kind Token.String tok then |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
141 |
output_syms s |> enclose |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
142 |
(enclose_literal "\"" "{\\isachardoublequoteopen}") |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
143 |
(enclose_literal "\"" "{\\isachardoublequoteclose}") |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset
|
144 |
else if Token.is_kind Token.AltString tok then |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
145 |
output_syms s |> enclose |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
146 |
(enclose_literal "`" "{\\isacharbackquoteopen}") |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
147 |
(enclose_literal "`" "{\\isacharbackquoteclose}") |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset
|
148 |
else if Token.is_kind Token.Verbatim tok then |
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset
|
149 |
let |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset
|
150 |
val (txt, pos) = Token.source_position_of tok; |
30642 | 151 |
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); |
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset
|
152 |
val out = implode (map output_syms_antiq ants); |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
153 |
in |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
154 |
out |> enclose |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
155 |
(enclose_literal "{*" "{\\isacharverbatimopen}") |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
156 |
(enclose_literal "*}" "{\\isacharverbatimclose}") |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
157 |
end |
17081 | 158 |
else output_syms s |
159 |
end; |
|
160 |
||
161 |
fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"; |
|
7745 | 162 |
|
17081 | 163 |
fun output_markup_env cmd txt = |
164 |
"%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ |
|
165 |
Symbol.strip_blanks txt ^ |
|
166 |
"%\n\\end{isamarkup" ^ cmd ^ "}%\n"; |
|
7756 | 167 |
|
17081 | 168 |
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
|
169 |
|
17081 | 170 |
val markup_true = "\\isamarkuptrue%\n"; |
171 |
val markup_false = "\\isamarkupfalse%\n"; |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
172 |
|
17081 | 173 |
val begin_delim = enclose "%\n\\isadelim" "\n"; |
174 |
val end_delim = enclose "%\n\\endisadelim" "\n"; |
|
175 |
val begin_tag = enclose "%\n\\isatag" "\n"; |
|
176 |
fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg; |
|
11860 | 177 |
|
178 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
179 |
(* theory presentation *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
180 |
|
9707 | 181 |
val tex_trailer = |
182 |
"%%% Local Variables:\n\ |
|
9135 | 183 |
\%%% mode: latex\n\ |
184 |
\%%% TeX-master: \"root\"\n\ |
|
9144 | 185 |
\%%% End:\n"; |
8192 | 186 |
|
9916 | 187 |
fun isabelle_file name txt = |
188 |
"%\n\\begin{isabellebody}%\n\ |
|
10247 | 189 |
\\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ |
9916 | 190 |
"\\end{isabellebody}%\n" ^ tex_trailer; |
9707 | 191 |
|
14924 | 192 |
fun symbol_source known name syms = isabelle_file name |
193 |
("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^ |
|
194 |
output_known_symbols known syms); |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
195 |
|
9038
63d20536971f
session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents:
8965
diff
changeset
|
196 |
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n"; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
197 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
198 |
|
8460 | 199 |
(* print mode *) |
200 |
||
8965 | 201 |
val latexN = "latex"; |
17218 | 202 |
val modes = [latexN, Symbol.xsymbolsN]; |
8965 | 203 |
|
8460 | 204 |
fun latex_output str = |
205 |
let val syms = Symbol.explode str |
|
23621 | 206 |
in (output_symbols syms, Symbol.length syms) end; |
19265 | 207 |
|
23621 | 208 |
fun latex_markup (s, _) = |
45666 | 209 |
if s = Isabelle_Markup.keywordN then ("\\isakeyword{", "}") |
210 |
else if s = Isabelle_Markup.commandN then ("\\isacommand{", "}") |
|
29325 | 211 |
else Markup.no_output; |
10955 | 212 |
|
23621 | 213 |
fun latex_indent "" _ = "" |
214 |
| latex_indent s _ = enclose "\\isaindent{" "}" s; |
|
215 |
||
216 |
val _ = Output.add_mode latexN latex_output Symbol.encode_raw; |
|
23703 | 217 |
val _ = Markup.add_mode latexN latex_markup; |
218 |
val _ = Pretty.add_mode latexN latex_indent; |
|
8460 | 219 |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
220 |
end; |