author | wenzelm |
Tue, 25 May 2021 21:44:01 +0200 | |
changeset 73779 | 546e1e591635 |
parent 73763 | eccc4a13216d |
child 73780 | 466fae6bf22e |
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 |
73754 | 2 |
Author: Makarius |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
3 |
|
73754 | 4 |
LaTeX output of theory sources. |
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 |
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
9 |
type text |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
10 |
val string: string -> text |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
11 |
val text: string * Position.T -> text |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
12 |
val block: text list -> text |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
13 |
val enclose_body: string -> string -> text list -> text list |
67462 | 14 |
val enclose_block: string -> string -> text list -> text |
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
15 |
val output_text: text list -> string |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
16 |
val output_positions: Position.T -> text list -> string |
67145 | 17 |
val output_name: string -> string |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
18 |
val output_ascii: string -> string |
71899 | 19 |
val output_ascii_breakable: string -> string -> string |
11719 | 20 |
val output_symbols: Symbol.symbol list -> string |
67145 | 21 |
val output_syms: string -> string |
67461 | 22 |
val symbols: Symbol_Pos.T list -> text |
23 |
val symbols_output: Symbol_Pos.T list -> text |
|
17081 | 24 |
val begin_delim: string -> string |
25 |
val end_delim: string -> string |
|
26 |
val begin_tag: string -> string |
|
27 |
val end_tag: string -> string |
|
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
28 |
val environment_block: string -> text list -> text |
61462 | 29 |
val environment: string -> string -> string |
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
30 |
val isabelle_body: string -> text list -> text list |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
31 |
val theory_entry: string -> string |
73754 | 32 |
val index_escape: string -> string |
33 |
type index_item = {text: text, like: string} |
|
34 |
type index_entry = {items: index_item list, def: bool} |
|
35 |
val index_entry: index_entry -> text |
|
73763
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
36 |
val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a |
66021 | 37 |
val latexN: string |
69346
3c29edccf739
expose latex mode operations, to facilitate adhoc changes to it;
wenzelm
parents:
67462
diff
changeset
|
38 |
val latex_output: string -> string * int |
3c29edccf739
expose latex mode operations, to facilitate adhoc changes to it;
wenzelm
parents:
67462
diff
changeset
|
39 |
val latex_markup: string * Properties.T -> Markup.output |
3c29edccf739
expose latex mode operations, to facilitate adhoc changes to it;
wenzelm
parents:
67462
diff
changeset
|
40 |
val latex_indent: string -> int -> string |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
41 |
end; |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
42 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
43 |
structure Latex: LATEX = |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
44 |
struct |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
45 |
|
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
46 |
(* text with positions *) |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
47 |
|
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
48 |
abstype text = Text of string * Position.T | Block of text list |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
49 |
with |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
50 |
|
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
51 |
fun string s = Text (s, Position.none); |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
52 |
val text = Text; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
53 |
val block = Block; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
54 |
|
73754 | 55 |
fun map_text f (Text (s, pos)) = Text (f s, pos) |
56 |
| map_text f (Block texts) = Block ((map o map_text) f texts); |
|
57 |
||
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
58 |
fun output_text texts = |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
59 |
let |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
60 |
fun output (Text (s, _)) = Buffer.add s |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
61 |
| output (Block body) = fold output body; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
62 |
in Buffer.empty |> fold output texts |> Buffer.content end; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
63 |
|
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
64 |
fun output_positions file_pos texts = |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
65 |
let |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
66 |
fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b); |
67195 | 67 |
fun add_position p positions = |
68 |
let val s = position (apply2 Value.print_int p) |
|
69 |
in positions |> s <> hd positions ? cons s end; |
|
70 |
||
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
71 |
fun output (Text (s, pos)) (positions, line) = |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
72 |
let |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
73 |
val positions' = |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
74 |
(case Position.line_of pos of |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
75 |
NONE => positions |
67195 | 76 |
| SOME l => add_position (line, l) positions); |
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
77 |
val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
78 |
in (positions', line') end |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
79 |
| output (Block body) res = fold output body res; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
80 |
in |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
81 |
(case Position.file_of file_pos of |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
82 |
NONE => "" |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
83 |
| SOME file => |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
84 |
([position (Markup.fileN, file), "\\endinput"], 1) |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
85 |
|> fold output texts |> #1 |> rev |> cat_lines) |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
86 |
end; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
87 |
|
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
88 |
end; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
89 |
|
67355 | 90 |
fun enclose_body bg en body = |
91 |
(if bg = "" then [] else [string bg]) @ body @ |
|
92 |
(if en = "" then [] else [string en]); |
|
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
93 |
|
67462 | 94 |
fun enclose_block bg en = block o enclose_body bg en; |
95 |
||
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
96 |
|
67145 | 97 |
(* output name for LaTeX macros *) |
98 |
||
99 |
val output_name = |
|
100 |
translate_string |
|
101 |
(fn "_" => "UNDERSCORE" |
|
102 |
| "'" => "PRIME" |
|
103 |
| "0" => "ZERO" |
|
104 |
| "1" => "ONE" |
|
105 |
| "2" => "TWO" |
|
106 |
| "3" => "THREE" |
|
107 |
| "4" => "FOUR" |
|
108 |
| "5" => "FIVE" |
|
109 |
| "6" => "SIX" |
|
110 |
| "7" => "SEVEN" |
|
111 |
| "8" => "EIGHT" |
|
112 |
| "9" => "NINE" |
|
113 |
| s => s); |
|
114 |
||
115 |
fun enclose_name bg en = enclose bg en o output_name; |
|
116 |
||
117 |
||
61455 | 118 |
(* output verbatim ASCII *) |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
119 |
|
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
120 |
val output_ascii = |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
121 |
translate_string |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
122 |
(fn " " => "\\ " |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
123 |
| "\t" => "\\ " |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
124 |
| "\n" => "\\isanewline\n" |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
125 |
| s => |
72315
8162ca81ea8a
suppress ligatures more robustly, notably for lualatex;
wenzelm
parents:
71899
diff
changeset
|
126 |
s |
8162ca81ea8a
suppress ligatures more robustly, notably for lualatex;
wenzelm
parents:
71899
diff
changeset
|
127 |
|> exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" ? enclose "{\\char`\\" "}" |
8162ca81ea8a
suppress ligatures more robustly, notably for lualatex;
wenzelm
parents:
71899
diff
changeset
|
128 |
|> suffix "{\\kern0pt}"); |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
129 |
|
71899 | 130 |
fun output_ascii_breakable sep = |
131 |
space_explode sep |
|
132 |
#> map output_ascii |
|
133 |
#> space_implode (output_ascii sep ^ "\\discretionary{}{}{}"); |
|
134 |
||
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset
|
135 |
|
61455 | 136 |
(* output symbols *) |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
137 |
|
7900 | 138 |
local |
139 |
||
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
140 |
val char_table = |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
141 |
Symtab.make |
63590
4854f7ee0987
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents:
61595
diff
changeset
|
142 |
[("\007", "{\\isacharbell}"), |
4854f7ee0987
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents:
61595
diff
changeset
|
143 |
("!", "{\\isacharbang}"), |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
144 |
("\"", "{\\isachardoublequote}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
145 |
("#", "{\\isacharhash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
146 |
("$", "{\\isachardollar}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
147 |
("%", "{\\isacharpercent}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
148 |
("&", "{\\isacharampersand}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
149 |
("'", "{\\isacharprime}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
150 |
("(", "{\\isacharparenleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
151 |
(")", "{\\isacharparenright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
152 |
("*", "{\\isacharasterisk}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
153 |
("+", "{\\isacharplus}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
154 |
(",", "{\\isacharcomma}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
155 |
("-", "{\\isacharminus}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
156 |
(".", "{\\isachardot}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
157 |
("/", "{\\isacharslash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
158 |
(":", "{\\isacharcolon}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
159 |
(";", "{\\isacharsemicolon}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
160 |
("<", "{\\isacharless}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
161 |
("=", "{\\isacharequal}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
162 |
(">", "{\\isachargreater}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
163 |
("?", "{\\isacharquery}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
164 |
("@", "{\\isacharat}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
165 |
("[", "{\\isacharbrackleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
166 |
("\\", "{\\isacharbackslash}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
167 |
("]", "{\\isacharbrackright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
168 |
("^", "{\\isacharcircum}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
169 |
("_", "{\\isacharunderscore}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
170 |
("`", "{\\isacharbackquote}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
171 |
("{", "{\\isacharbraceleft}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
172 |
("|", "{\\isacharbar}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
173 |
("}", "{\\isacharbraceright}"), |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
174 |
("~", "{\\isachartilde}")]; |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
175 |
|
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
176 |
fun output_chr " " = "\\ " |
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
43485
diff
changeset
|
177 |
| 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
|
178 |
| 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
|
179 |
| output_chr c = |
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
180 |
(case Symtab.lookup char_table c of |
72315
8162ca81ea8a
suppress ligatures more robustly, notably for lualatex;
wenzelm
parents:
71899
diff
changeset
|
181 |
SOME s => s ^ "{\\kern0pt}" |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset
|
182 |
| 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
|
183 |
|
67263 | 184 |
fun output_sym sym = |
14874 | 185 |
(case Symbol.decode sym of |
186 |
Symbol.Char s => output_chr s |
|
37533
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36959
diff
changeset
|
187 |
| Symbol.UTF8 s => s |
67263 | 188 |
| Symbol.Sym s => enclose_name "{\\isasym" "}" s |
189 |
| Symbol.Control s => enclose_name "\\isactrl" " " s |
|
43485 | 190 |
| Symbol.Malformed s => error (Symbol.malformed_msg s) |
191 |
| Symbol.EOF => error "Bad EOF symbol"); |
|
7900 | 192 |
|
67428 | 193 |
open Basic_Symbol_Pos; |
194 |
||
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
195 |
val scan_latex_length = |
67428 | 196 |
Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s) |
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
197 |
>> (Symbol.length o map Symbol_Pos.symbol) || |
67428 | 198 |
$$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0; |
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
199 |
|
67263 | 200 |
val scan_latex = |
67428 | 201 |
$$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " |
202 |
>> (implode o map Symbol_Pos.symbol) || |
|
67263 | 203 |
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol); |
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
204 |
|
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
205 |
fun read scan syms = |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
206 |
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
|
207 |
|
7900 | 208 |
in |
209 |
||
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
210 |
fun length_symbols syms = |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
211 |
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
|
212 |
|
67263 | 213 |
fun output_symbols syms = |
67428 | 214 |
if member (op =) syms Symbol.latex then |
67263 | 215 |
(case read scan_latex syms of |
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
216 |
SOME ss => implode ss |
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
217 |
| NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms))) |
67263 | 218 |
else implode (map output_sym syms); |
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset
|
219 |
|
8192 | 220 |
val output_syms = output_symbols o Symbol.explode; |
7900 | 221 |
|
222 |
end; |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
223 |
|
67461 | 224 |
fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms)); |
225 |
fun symbols_output syms = |
|
226 |
text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms)); |
|
227 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
228 |
|
61455 | 229 |
(* tags *) |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
230 |
|
67145 | 231 |
val begin_delim = enclose_name "%\n\\isadelim" "\n"; |
232 |
val end_delim = enclose_name "%\n\\endisadelim" "\n"; |
|
233 |
val begin_tag = enclose_name "%\n\\isatag" "\n"; |
|
234 |
fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg; |
|
11860 | 235 |
|
236 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
237 |
(* theory presentation *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
238 |
|
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
239 |
fun environment_delim name = |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
240 |
("%\n\\begin{" ^ output_name name ^ "}%\n", |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
241 |
"%\n\\end{" ^ output_name name ^ "}"); |
61462 | 242 |
|
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
243 |
fun environment_block name = environment_delim name |-> enclose_body #> block; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
244 |
fun environment name = environment_delim name |-> enclose; |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67189
diff
changeset
|
245 |
|
67263 | 246 |
fun isabelle_body name = |
247 |
enclose_body |
|
248 |
("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n") |
|
249 |
"%\n\\end{isabellebody}%\n"; |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
250 |
|
9038
63d20536971f
session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents:
8965
diff
changeset
|
251 |
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n"; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
252 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
253 |
|
73754 | 254 |
(* index entries *) |
255 |
||
256 |
type index_item = {text: text, like: string}; |
|
257 |
type index_entry = {items: index_item list, def: bool}; |
|
258 |
||
259 |
val index_escape = |
|
260 |
translate_string (fn s => |
|
73763
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
261 |
if member_string "!\"@|" s then "\\char" ^ string_of_int (ord s) |
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
262 |
else if member_string "\\{}#" s then "\"" ^ s else s); |
73754 | 263 |
|
264 |
fun index_item (item: index_item) = |
|
265 |
let |
|
266 |
val like_text = |
|
73779
546e1e591635
more direct index_entry: no positions required -- text is eventually moved to .ind file;
wenzelm
parents:
73763
diff
changeset
|
267 |
if #like item = "" then "" |
546e1e591635
more direct index_entry: no positions required -- text is eventually moved to .ind file;
wenzelm
parents:
73763
diff
changeset
|
268 |
else index_escape (#like item) ^ "@"; |
546e1e591635
more direct index_entry: no positions required -- text is eventually moved to .ind file;
wenzelm
parents:
73763
diff
changeset
|
269 |
val item_text = index_escape (output_text [#text item]); |
546e1e591635
more direct index_entry: no positions required -- text is eventually moved to .ind file;
wenzelm
parents:
73763
diff
changeset
|
270 |
in like_text ^ item_text end; |
73754 | 271 |
|
272 |
fun index_entry (entry: index_entry) = |
|
73779
546e1e591635
more direct index_entry: no positions required -- text is eventually moved to .ind file;
wenzelm
parents:
73763
diff
changeset
|
273 |
(space_implode "!" (map index_item (#items entry)) ^ |
546e1e591635
more direct index_entry: no positions required -- text is eventually moved to .ind file;
wenzelm
parents:
73763
diff
changeset
|
274 |
"|" ^ index_escape (if #def entry then "isaindexdef" else "isaindexref")) |
546e1e591635
more direct index_entry: no positions required -- text is eventually moved to .ind file;
wenzelm
parents:
73763
diff
changeset
|
275 |
|> enclose "\\index{" "}" |
546e1e591635
more direct index_entry: no positions required -- text is eventually moved to .ind file;
wenzelm
parents:
73763
diff
changeset
|
276 |
|> string; |
73754 | 277 |
|
73763
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
278 |
fun index_binding NONE = I |
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
279 |
| index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref")); |
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
280 |
|
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
281 |
fun index_variants setup binding = |
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
282 |
fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false]; |
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
283 |
|
eccc4a13216d
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents:
73754
diff
changeset
|
284 |
|
8460 | 285 |
(* print mode *) |
286 |
||
8965 | 287 |
val latexN = "latex"; |
288 |
||
8460 | 289 |
fun latex_output str = |
290 |
let val syms = Symbol.explode str |
|
64526
01920e390645
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset
|
291 |
in (output_symbols syms, length_symbols syms) end; |
19265 | 292 |
|
69346
3c29edccf739
expose latex mode operations, to facilitate adhoc changes to it;
wenzelm
parents:
67462
diff
changeset
|
293 |
fun latex_markup (s, _: Properties.T) = |
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset
|
294 |
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
|
295 |
then ("\\isacommand{", "}") |
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset
|
296 |
else if s = Markup.keyword2N |
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset
|
297 |
then ("\\isakeyword{", "}") |
29325 | 298 |
else Markup.no_output; |
10955 | 299 |
|
23621 | 300 |
fun latex_indent "" _ = "" |
301 |
| latex_indent s _ = enclose "\\isaindent{" "}" s; |
|
302 |
||
67428 | 303 |
val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche); |
23703 | 304 |
val _ = Markup.add_mode latexN latex_markup; |
305 |
val _ = Pretty.add_mode latexN latex_indent; |
|
8460 | 306 |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
307 |
end; |