author  wenzelm 
Sun, 02 Nov 2014 16:09:35 +0100  
changeset 58870  e2c0d8ef29cb 
parent 58861  5ff61774df11 
child 58978  e42da880c61e 
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 
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

9 
val output_ascii: string > string 
14924  10 
val output_known_symbols: (string > bool) * (string > bool) > 
11 
Symbol.symbol list > string 

11719  12 
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

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

16 
val output_verbatim: string > string 

17 
val markup_true: string 

18 
val markup_false: string 

19 
val begin_delim: string > string 

20 
val end_delim: string > string 

21 
val begin_tag: string > string 

22 
val end_tag: string > string 

9707  23 
val tex_trailer: string 
58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset

24 
val isabelle_theory: string > string > string 
14924  25 
val symbol_source: (string > bool) * (string > bool) > 
26 
string > Symbol.symbol list > string 

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

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

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

30 

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

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

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

33 

58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

34 
(* literal ASCII *) 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

35 

23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

36 
val output_ascii = 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

37 
translate_string 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

38 
(fn " " => "\\ " 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

39 
 "\t" => "\\ " 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

40 
 "\n" => "\\isanewline\n" 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

41 
 s => 
58727  42 
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

43 
then enclose "{\\char`\\" "}" s else s); 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

44 

23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

45 

7726
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 
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset

90 
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

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 
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset

99 
 Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym 
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset

100 
 Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s 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

101 
 Symbol.Raw s => s 
43485  102 
 Symbol.Malformed s => error (Symbol.malformed_msg s) 
103 
 Symbol.EOF => error "Bad EOF symbol"); 

7900  104 

105 
in 

106 

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

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

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

111 
val output_syms_antiq = 
30589  112 
(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

113 
 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

114 
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" 
53167  115 
(output_symbols (map Symbol_Pos.symbol ss))); 
22648
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset

116 

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

118 

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

119 

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

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

121 

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

123 
let val s = Token.content_of tok in 
58861
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58727
diff
changeset

124 
if Token.is_kind Token.Comment tok then "" 
46811
03a2dc9e0624
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents:
45666
diff
changeset

125 
else if Token.is_command tok then 
17081  126 
"\\isacommand{" ^ output_syms s ^ "}" 
50238
98d35a7368bd
more uniform Symbol.is_ascii_identifier in ML/Scala;
wenzelm
parents:
50201
diff
changeset

127 
else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then 
17081  128 
"\\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

129 
else if Token.is_kind Token.String tok then 
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset

130 
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (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

131 
else if Token.is_kind Token.AltString tok then 
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset

132 
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (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

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

134 
let 
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55750
diff
changeset

135 
val {text, pos, ...} = Token.source_position_of tok; 
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55750
diff
changeset

136 
val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos); 
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset

137 
val out = implode (map output_syms_antiq ants); 
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset

138 
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end 
55033  139 
else if Token.is_kind Token.Cartouche tok then 
140 
enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s) 

17081  141 
else output_syms s 
142 
end; 

143 

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

7745  145 

17081  146 
fun output_markup_env cmd txt = 
147 
"%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ 

148 
Symbol.strip_blanks txt ^ 

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

7756  150 

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

152 

17081  153 
val markup_true = "\\isamarkuptrue%\n"; 
154 
val markup_false = "\\isamarkupfalse%\n"; 

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

155 

17081  156 
val begin_delim = enclose "%\n\\isadelim" "\n"; 
157 
val end_delim = enclose "%\n\\endisadelim" "\n"; 

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

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

11860  160 

161 

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

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

163 

9707  164 
val tex_trailer = 
165 
"%%% Local Variables:\n\ 

9135  166 
\%%% mode: latex\n\ 
167 
\%%% TeXmaster: \"root\"\n\ 

9144  168 
\%%% End:\n"; 
8192  169 

58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset

170 
fun isabelle_theory name txt = 
9916  171 
"%\n\\begin{isabellebody}%\n\ 
58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset

172 
\\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ 
9916  173 
"\\end{isabellebody}%\n" ^ tex_trailer; 
9707  174 

58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset

175 
fun symbol_source known name syms = 
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset

176 
isabelle_theory name 
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset

177 
("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^ 
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset

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

179 

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

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

181 

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

182 

8460  183 
(* print mode *) 
184 

8965  185 
val latexN = "latex"; 
17218  186 
val modes = [latexN, Symbol.xsymbolsN]; 
8965  187 

8460  188 
fun latex_output str = 
189 
let val syms = Symbol.explode str 

23621  190 
in (output_symbols syms, Symbol.length syms) end; 
19265  191 

23621  192 
fun latex_markup (s, _) = 
55750
baa7a1e57f4a
back to Markup.command for actual tokens (amending 4a4e5686e091)  avoid conflict of jEdit token marker with Rendering.text_colors;
wenzelm
parents:
55744
diff
changeset

193 
if s = Markup.commandN orelse s = Markup.keyword1N then ("\\isacommand{", "}") 
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55033
diff
changeset

194 
else if s = Markup.keyword2N then ("\\isakeyword{", "}") 
29325  195 
else Markup.no_output; 
10955  196 

23621  197 
fun latex_indent "" _ = "" 
198 
 latex_indent s _ = enclose "\\isaindent{" "}" s; 

199 

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

23703  201 
val _ = Markup.add_mode latexN latex_markup; 
202 
val _ = Pretty.add_mode latexN latex_indent; 

8460  203 

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

204 
end; 