author | wenzelm |
Sat, 29 May 2004 15:08:21 +0200 | |
changeset 14840 | dc23ff2629e2 |
parent 14680 | 6029e76841fd |
child 14874 | 23c73484312f |
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 |
ID: $Id$ |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
8808 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
5 |
|
8460 | 6 |
LaTeX presentation primitives (based on outer lexical syntax). |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
7 |
*) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
8 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
9 |
signature LATEX = |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
10 |
sig |
11719 | 11 |
val output_symbols: Symbol.symbol list -> string |
9135 | 12 |
datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim |
13 |
val output_tokens: (token * string) list -> string |
|
11860 | 14 |
val flag_markup: bool -> string |
9707 | 15 |
val tex_trailer: string |
9916 | 16 |
val isabelle_file: string -> string -> string |
8499 | 17 |
val old_symbol_source: string -> Symbol.symbol list -> string |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
18 |
val theory_entry: string -> string |
9135 | 19 |
val modes: string list |
8965 | 20 |
val setup: (theory -> theory) list |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
21 |
end; |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
22 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
23 |
structure Latex: LATEX = |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
24 |
struct |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
25 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
26 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
27 |
(* symbol output *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
28 |
|
7900 | 29 |
local |
30 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
31 |
val output_chr = fn |
9505 | 32 |
" " => "\\ " | |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
33 |
"\n" => "\\isanewline\n" | |
9668 | 34 |
"!" => "{\\isacharbang}" | |
35 |
"\"" => "{\\isachardoublequote}" | |
|
9663 | 36 |
"#" => "{\\isacharhash}" | |
37 |
"$" => "{\\isachardollar}" | |
|
38 |
"%" => "{\\isacharpercent}" | |
|
39 |
"&" => "{\\isacharampersand}" | |
|
40 |
"'" => "{\\isacharprime}" | |
|
41 |
"(" => "{\\isacharparenleft}" | |
|
42 |
")" => "{\\isacharparenright}" | |
|
43 |
"*" => "{\\isacharasterisk}" | |
|
9668 | 44 |
"+" => "{\\isacharplus}" | |
45 |
"," => "{\\isacharcomma}" | |
|
9663 | 46 |
"-" => "{\\isacharminus}" | |
9668 | 47 |
"." => "{\\isachardot}" | |
48 |
"/" => "{\\isacharslash}" | |
|
49 |
":" => "{\\isacharcolon}" | |
|
50 |
";" => "{\\isacharsemicolon}" | |
|
9663 | 51 |
"<" => "{\\isacharless}" | |
9668 | 52 |
"=" => "{\\isacharequal}" | |
9663 | 53 |
">" => "{\\isachargreater}" | |
9668 | 54 |
"?" => "{\\isacharquery}" | |
55 |
"@" => "{\\isacharat}" | |
|
9663 | 56 |
"[" => "{\\isacharbrackleft}" | |
57 |
"\\" => "{\\isacharbackslash}" | |
|
58 |
"]" => "{\\isacharbrackright}" | |
|
59 |
"^" => "{\\isacharcircum}" | |
|
60 |
"_" => "{\\isacharunderscore}" | |
|
9668 | 61 |
"`" => "{\\isacharbackquote}" | |
9663 | 62 |
"{" => "{\\isacharbraceleft}" | |
63 |
"|" => "{\\isacharbar}" | |
|
64 |
"}" => "{\\isacharbraceright}" | |
|
65 |
"~" => "{\\isachartilde}" | |
|
10184 | 66 |
c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
67 |
|
7900 | 68 |
fun output_sym s = |
14840 | 69 |
if Symbol.is_char s then output_chr s |
70 |
else if Symbol.is_raw s then Symbol.decode_raw s |
|
71 |
else if String.isPrefix "\\<^" s then |
|
72 |
enclose "\\isactrl" " " (String.substring (s, 3, size s - 4)) |
|
73 |
else if String.isPrefix "\\<" s then |
|
74 |
enclose "{\\isasym" "}" (String.substring (s, 2, size s - 3)) |
|
75 |
else sys_error "output_sym"; |
|
7900 | 76 |
|
77 |
in |
|
78 |
||
8192 | 79 |
val output_symbols = implode o map output_sym; |
80 |
val output_syms = output_symbols o Symbol.explode; |
|
7900 | 81 |
|
82 |
end; |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
83 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
84 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
85 |
(* token output *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
86 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
87 |
structure T = OuterLex; |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
88 |
|
8660 | 89 |
datatype token = |
90 |
Basic of T.token | |
|
9135 | 91 |
Markup of string | |
92 |
MarkupEnv of string | |
|
93 |
Verbatim; |
|
7756 | 94 |
|
95 |
||
96 |
val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment; |
|
97 |
||
9135 | 98 |
fun output_tok (Basic tok, _) = |
7752 | 99 |
let val s = T.val_of tok in |
7756 | 100 |
if invisible_token tok then "" |
7800 | 101 |
else if T.is_kind T.Command tok then |
9668 | 102 |
"\\isacommand{" ^ output_syms s ^ "}" |
14680 | 103 |
else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then |
7900 | 104 |
"\\isakeyword{" ^ output_syms s ^ "}" |
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14561
diff
changeset
|
105 |
else if T.is_kind T.String tok then output_syms (Library.quote s) |
7900 | 106 |
else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s) |
107 |
else output_syms s |
|
7756 | 108 |
end |
11012 | 109 |
| output_tok (Markup cmd, txt) = |
110 |
"%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n" |
|
9135 | 111 |
| output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ |
11012 | 112 |
Symbol.strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n" |
113 |
| output_tok (Verbatim, txt) = "%\n" ^ Symbol.strip_blanks txt ^ "\n"; |
|
7745 | 114 |
|
7756 | 115 |
|
116 |
val output_tokens = implode o map output_tok; |
|
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
117 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
118 |
|
11860 | 119 |
fun flag_markup true = "\\isamarkuptrue%\n" |
120 |
| flag_markup false = "\\isamarkupfalse%\n"; |
|
121 |
||
122 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
123 |
(* theory presentation *) |
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
124 |
|
9707 | 125 |
val tex_trailer = |
126 |
"%%% Local Variables:\n\ |
|
9135 | 127 |
\%%% mode: latex\n\ |
128 |
\%%% TeX-master: \"root\"\n\ |
|
9144 | 129 |
\%%% End:\n"; |
8192 | 130 |
|
9916 | 131 |
fun isabelle_file name txt = |
132 |
"%\n\\begin{isabellebody}%\n\ |
|
10247 | 133 |
\\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ |
9916 | 134 |
"\\end{isabellebody}%\n" ^ tex_trailer; |
9707 | 135 |
|
8499 | 136 |
fun old_symbol_source name syms = |
9916 | 137 |
isabelle_file name ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms); |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
138 |
|
9038
63d20536971f
session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents:
8965
diff
changeset
|
139 |
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n"; |
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
140 |
|
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
141 |
|
8460 | 142 |
(* print mode *) |
143 |
||
8965 | 144 |
val latexN = "latex"; |
9135 | 145 |
val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN]; |
8965 | 146 |
|
8460 | 147 |
fun latex_output str = |
148 |
let val syms = Symbol.explode str |
|
149 |
in (output_symbols syms, real (Symbol.length syms)) end; |
|
150 |
||
10955 | 151 |
fun latex_indent "" = "" |
152 |
| latex_indent s = enclose "\\isaindent{" "}" s; |
|
153 |
||
9558 | 154 |
val token_translation = |
9749
36ddd544a18d
token trans: removed \mbox to achieve proper italic correction;
wenzelm
parents:
9707
diff
changeset
|
155 |
map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes; |
8965 | 156 |
|
14840 | 157 |
val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.default_raw); |
8965 | 158 |
val setup = [Theory.add_tokentrfuns token_translation]; |
8460 | 159 |
|
160 |
||
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset
|
161 |
end; |