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