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