author  wenzelm 
Mon, 29 Aug 2011 21:55:49 +0200  
changeset 44574  24444588fddd 
parent 43709  717e96cf9527 
child 45666  d83797ef0d2d 
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 " " = "\\ " 
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
43485
diff
changeset

86 
 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

87 
 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

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

89 
(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

90 
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

91 
 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

92 

14924  93 
val output_chrs = translate_string output_chr; 
94 

95 
fun output_known_sym (known_sym, known_ctrl) sym = 

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

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

98 
 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

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

100 
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

101 
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

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

103 
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

104 
else output_chrs sym 
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40402
diff
changeset

105 
 Symbol.Raw s => s 
43485  106 
 Symbol.Malformed s => error (Symbol.malformed_msg s) 
107 
 Symbol.EOF => error "Bad EOF symbol"); 

7900  108 

109 
in 

110 

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

8192  113 
val output_syms = output_symbols o Symbol.explode; 
7900  114 

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

115 
val output_syms_antiq = 
30589  116 
(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

117 
 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

118 
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

119 
(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

120 
 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

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

122 

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

124 

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

125 

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

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

127 

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 
val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment; 
7756  129 

17081  130 
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

131 
let val s = Token.content_of tok in 
17081  132 
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

133 
else if Token.is_kind Token.Command tok then 
17081  134 
"\\isacommand{" ^ output_syms s ^ "}" 
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40523
diff
changeset

135 
else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then 
17081  136 
"\\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

137 
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

138 
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

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

140 
(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

141 
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

142 
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

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

144 
(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

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

146 
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

147 
val (txt, pos) = Token.source_position_of tok; 
30642  148 
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

149 
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

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

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

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

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

154 
end 
17081  155 
else output_syms s 
156 
end; 

157 

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

7745  159 

17081  160 
fun output_markup_env cmd txt = 
161 
"%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ 

162 
Symbol.strip_blanks txt ^ 

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

7756  164 

17081  165 
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

166 

17081  167 
val markup_true = "\\isamarkuptrue%\n"; 
168 
val markup_false = "\\isamarkupfalse%\n"; 

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

169 

17081  170 
val begin_delim = enclose "%\n\\isadelim" "\n"; 
171 
val end_delim = enclose "%\n\\endisadelim" "\n"; 

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

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

11860  174 

175 

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

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

177 

9707  178 
val tex_trailer = 
179 
"%%% Local Variables:\n\ 

9135  180 
\%%% mode: latex\n\ 
181 
\%%% TeXmaster: \"root\"\n\ 

9144  182 
\%%% End:\n"; 
8192  183 

9916  184 
fun isabelle_file name txt = 
185 
"%\n\\begin{isabellebody}%\n\ 

10247  186 
\\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ 
9916  187 
"\\end{isabellebody}%\n" ^ tex_trailer; 
9707  188 

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

191 
output_known_symbols known syms); 

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

192 

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

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

194 

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

195 

8460  196 
(* print mode *) 
197 

8965  198 
val latexN = "latex"; 
17218  199 
val modes = [latexN, Symbol.xsymbolsN]; 
8965  200 

8460  201 
fun latex_output str = 
202 
let val syms = Symbol.explode str 

23621  203 
in (output_symbols syms, Symbol.length syms) end; 
19265  204 

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

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

29325  208 
else Markup.no_output; 
10955  209 

23621  210 
fun latex_indent "" _ = "" 
211 
 latex_indent s _ = enclose "\\isaindent{" "}" s; 

212 

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

23703  214 
val _ = Markup.add_mode latexN latex_markup; 
215 
val _ = Pretty.add_mode latexN latex_indent; 

8460  216 

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

217 
end; 