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