author  wenzelm 
Sun, 07 Nov 2010 22:51:16 +0100  
changeset 40402  b646316f8b3c 
parent 39666  4f628ee48fd7 
child 40523  1050315f6ee2 
permissions  rwrr 
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 
14924  9 
val output_known_symbols: (string > bool) * (string > bool) > 
10 
Symbol.symbol list > string 

11719  11 
val output_symbols: Symbol.symbol list > string 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

12 
val output_basic: Token.T > string 
17081  13 
val output_markup: string > string > string 
14 
val output_markup_env: string > string > string 

15 
val output_verbatim: string > string 

16 
val markup_true: string 

17 
val markup_false: string 

18 
val begin_delim: string > string 

19 
val end_delim: string > string 

20 
val begin_tag: string > string 

21 
val end_tag: string > string 

9707  22 
val tex_trailer: string 
9916  23 
val isabelle_file: string > string > string 
14924  24 
val symbol_source: (string > bool) * (string > bool) > 
25 
string > Symbol.symbol list > string 

7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

26 
val theory_entry: string > string 
9135  27 
val modes: string list 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

28 
end; 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

29 

2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

30 
structure Latex: LATEX = 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

31 
struct 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

32 

40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

33 
(* literal text *) 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

34 

b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

35 
local 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

36 
val hex = Int.fmt StringCvt.HEX; 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

37 
fun hex_byte c = hex (ord c div 16) ^ hex (ord c mod 16); 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

38 
in 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

39 

b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

40 
fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}"; 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

41 
fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg); 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

42 

b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

43 
end; 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

44 

7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

45 

2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

46 
(* symbol output *) 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

47 

7900  48 
local 
49 

40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

50 
val char_table = 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

51 
Symtab.make 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

52 
[("!", "{\\isacharbang}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

53 
("\"", "{\\isachardoublequote}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

54 
("#", "{\\isacharhash}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

55 
("$", "{\\isachardollar}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

56 
("%", "{\\isacharpercent}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

57 
("&", "{\\isacharampersand}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

58 
("'", "{\\isacharprime}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

59 
("(", "{\\isacharparenleft}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

60 
(")", "{\\isacharparenright}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

61 
("*", "{\\isacharasterisk}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

62 
("+", "{\\isacharplus}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

63 
(",", "{\\isacharcomma}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

64 
("", "{\\isacharminus}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

65 
(".", "{\\isachardot}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

66 
("/", "{\\isacharslash}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

67 
(":", "{\\isacharcolon}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

68 
(";", "{\\isacharsemicolon}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

69 
("<", "{\\isacharless}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

70 
("=", "{\\isacharequal}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

71 
(">", "{\\isachargreater}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

72 
("?", "{\\isacharquery}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

73 
("@", "{\\isacharat}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

74 
("[", "{\\isacharbrackleft}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

75 
("\\", "{\\isacharbackslash}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

76 
("]", "{\\isacharbrackright}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

77 
("^", "{\\isacharcircum}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

78 
("_", "{\\isacharunderscore}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

79 
("`", "{\\isacharbackquote}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

80 
("{", "{\\isacharbraceleft}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

81 
("", "{\\isacharbar}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

82 
("}", "{\\isacharbraceright}"), 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

83 
("~", "{\\isachartilde}")]; 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

84 

b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

85 
fun output_chr " " = "\\ " 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

86 
 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

87 
 output_chr c = 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

88 
(case Symtab.lookup char_table c of 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

89 
SOME s => enclose_literal c s 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

90 
 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

91 

14924  92 
val output_chrs = translate_string output_chr; 
93 

94 
fun output_known_sym (known_sym, known_ctrl) sym = 

14874  95 
(case Symbol.decode sym of 
96 
Symbol.Char s => output_chr s 

37533
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36959
diff
changeset

97 
 Symbol.UTF8 s => s 
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

98 
 Symbol.Sym s => 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

99 
if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s) 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

100 
else output_chrs sym 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

101 
 Symbol.Ctrl s => 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

102 
if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

103 
else output_chrs sym 
14874  104 
 Symbol.Raw s => s); 
7900  105 

106 
in 

107 

14924  108 
val output_known_symbols = implode oo (map o output_known_sym); 
109 
val output_symbols = output_known_symbols (K true, K true); 

8192  110 
val output_syms = output_symbols o Symbol.explode; 
7900  111 

27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset

112 
val output_syms_antiq = 
30589  113 
(fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss) 
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset

114 
 Antiquote.Antiq (ss, _) => 
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

115 
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

116 
(output_symbols (map Symbol_Pos.symbol ss)) 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

117 
 Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}" 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

118 
 Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}"); 
22648
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset

119 

7900  120 
end; 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

121 

2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

122 

2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

123 
(* token output *) 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

124 

36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

125 
val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment; 
7756  126 

17081  127 
fun output_basic tok = 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

128 
let val s = Token.content_of tok in 
17081  129 
if invisible_token tok then "" 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

130 
else if Token.is_kind Token.Command tok then 
17081  131 
"\\isacommand{" ^ output_syms s ^ "}" 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

132 
else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then 
17081  133 
"\\isakeyword{" ^ output_syms s ^ "}" 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

134 
else if Token.is_kind Token.String tok then 
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

135 
output_syms s > enclose 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

136 
(enclose_literal "\"" "{\\isachardoublequoteopen}") 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

137 
(enclose_literal "\"" "{\\isachardoublequoteclose}") 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

138 
else if Token.is_kind Token.AltString tok then 
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

139 
output_syms s > enclose 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

140 
(enclose_literal "`" "{\\isacharbackquoteopen}") 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

141 
(enclose_literal "`" "{\\isacharbackquoteclose}") 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

142 
else if Token.is_kind Token.Verbatim tok then 
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset

143 
let 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
30642
diff
changeset

144 
val (txt, pos) = Token.source_position_of tok; 
30642  145 
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); 
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset

146 
val out = implode (map output_syms_antiq ants); 
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

147 
in 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

148 
out > enclose 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

149 
(enclose_literal "{*" "{\\isacharverbatimopen}") 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

150 
(enclose_literal "*}" "{\\isacharverbatimclose}") 
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

151 
end 
17081  152 
else output_syms s 
153 
end; 

154 

155 
fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"; 

7745  156 

17081  157 
fun output_markup_env cmd txt = 
158 
"%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ 

159 
Symbol.strip_blanks txt ^ 

160 
"%\n\\end{isamarkup" ^ cmd ^ "}%\n"; 

7756  161 

17081  162 
fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n"; 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

163 

17081  164 
val markup_true = "\\isamarkuptrue%\n"; 
165 
val markup_false = "\\isamarkupfalse%\n"; 

7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

166 

17081  167 
val begin_delim = enclose "%\n\\isadelim" "\n"; 
168 
val end_delim = enclose "%\n\\endisadelim" "\n"; 

169 
val begin_tag = enclose "%\n\\isatag" "\n"; 

170 
fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg; 

11860  171 

172 

7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

173 
(* theory presentation *) 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

174 

9707  175 
val tex_trailer = 
176 
"%%% Local Variables:\n\ 

9135  177 
\%%% mode: latex\n\ 
178 
\%%% TeXmaster: \"root\"\n\ 

9144  179 
\%%% End:\n"; 
8192  180 

9916  181 
fun isabelle_file name txt = 
182 
"%\n\\begin{isabellebody}%\n\ 

10247  183 
\\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ 
9916  184 
"\\end{isabellebody}%\n" ^ tex_trailer; 
9707  185 

14924  186 
fun symbol_source known name syms = isabelle_file name 
187 
("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^ 

188 
output_known_symbols known syms); 

7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

189 

9038
63d20536971f
session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents:
8965
diff
changeset

190 
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n"; 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

191 

2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

192 

8460  193 
(* print mode *) 
194 

8965  195 
val latexN = "latex"; 
17218  196 
val modes = [latexN, Symbol.xsymbolsN]; 
8965  197 

8460  198 
fun latex_output str = 
199 
let val syms = Symbol.explode str 

23621  200 
in (output_symbols syms, Symbol.length syms) end; 
19265  201 

23621  202 
fun latex_markup (s, _) = 
203 
if s = Markup.keywordN then ("\\isakeyword{", "}") 

204 
else if s = Markup.commandN then ("\\isacommand{", "}") 

29325  205 
else Markup.no_output; 
10955  206 

23621  207 
fun latex_indent "" _ = "" 
208 
 latex_indent s _ = enclose "\\isaindent{" "}" s; 

209 

210 
val _ = Output.add_mode latexN latex_output Symbol.encode_raw; 

23703  211 
val _ = Markup.add_mode latexN latex_markup; 
212 
val _ = Pretty.add_mode latexN latex_indent; 

8460  213 

7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

214 
end; 