author  wenzelm 
Sun, 27 Nov 2016 13:13:26 +0100  
changeset 64526  01920e390645 
parent 63936  b87784e19a77 
child 66020  a31760eee09d 
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 
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

10 
val latex_control: Symbol.symbol 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

11 
val is_latex_control: Symbol.symbol > bool 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

12 
val embed_raw: string > string 
14924  13 
val output_known_symbols: (string > bool) * (string > bool) > 
14 
Symbol.symbol list > string 

11719  15 
val output_symbols: Symbol.symbol list > string 
61455  16 
val output_token: Token.T > string 
17081  17 
val begin_delim: string > string 
18 
val end_delim: string > string 

19 
val begin_tag: string > string 

20 
val end_tag: string > string 

61462  21 
val environment: string > string > string 
9707  22 
val tex_trailer: string 
58870
e2c0d8ef29cb
more flexibile \setisabellecontext, independently of header;
wenzelm
parents:
58861
diff
changeset

23 
val isabelle_theory: 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 

61455  33 
(* output verbatim ASCII *) 
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
55828
diff
changeset

34 

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

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

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

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

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

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

40 
 s => 
61578  41 
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

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

43 

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

44 

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

46 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

47 
val latex_control = "\<^latex>"; 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

48 
fun is_latex_control s = s = latex_control; 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

49 

aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

50 
val embed_raw = prefix latex_control o cartouche; 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

51 

7900  52 
local 
53 

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

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

55 
Symtab.make 
63590
4854f7ee0987
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents:
61595
diff
changeset

56 
[("\007", "{\\isacharbell}"), 
4854f7ee0987
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents:
61595
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

89 

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

90 
fun output_chr " " = "\\ " 
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
43485
diff
changeset

91 
 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

92 
 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

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

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

95 
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

96 
 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

97 

14924  98 
val output_chrs = translate_string output_chr; 
99 

100 
fun output_known_sym (known_sym, known_ctrl) sym = 

14874  101 
(case Symbol.decode sym of 
102 
Symbol.Char s => output_chr s 

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

103 
 Symbol.UTF8 s => s 
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset

104 
 Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym 
61475  105 
 Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym 
43485  106 
 Symbol.Malformed s => error (Symbol.malformed_msg s) 
107 
 Symbol.EOF => error "Bad EOF symbol"); 

7900  108 

64526
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

109 
val scan_latex_length = 
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

110 
Scan.many1 (fn (s, _) => Symbol.not_eof s andalso not (is_latex_control s)) 
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

111 
>> (Symbol.length o map Symbol_Pos.symbol)  
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

112 
Scan.one (is_latex_control o Symbol_Pos.symbol)  
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

113 
Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0; 
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

114 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

115 
fun scan_latex known = 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

116 
Scan.one (is_latex_control o Symbol_Pos.symbol)  
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

117 
Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol)  
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

118 
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol); 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

119 

64526
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

120 
fun read scan syms = 
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

121 
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

122 

7900  123 
in 
124 

64526
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

125 
fun length_symbols syms = 
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

126 
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

127 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

128 
fun output_known_symbols known syms = 
64526
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

129 
if exists is_latex_control syms then 
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

130 
(case read (scan_latex known) syms of 
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

131 
SOME ss => implode ss 
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

132 
 NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms))) 
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

133 
else implode (map (output_known_sym known) syms); 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

134 

14924  135 
val output_symbols = output_known_symbols (K true, K true); 
8192  136 
val output_syms = output_symbols o Symbol.explode; 
7900  137 

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

138 
val output_syms_antiq = 
30589  139 
(fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss) 
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset

140 
 Antiquote.Control {name = (name, _), body, ...} => 
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset

141 
"\\isaantiqcontrol{" ^ output_symbols (Symbol.explode name) ^ "}" ^ 
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset

142 
output_symbols (map Symbol_Pos.symbol body) 
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset

143 
 Antiquote.Antiq {body, ...} => 
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39666
diff
changeset

144 
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" 
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset

145 
(output_symbols (map Symbol_Pos.symbol body))); 
22648
8c6b4f7548e3
output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents:
19265
diff
changeset

146 

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

148 

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

149 

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

151 

61455  152 
fun output_token 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

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

154 
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

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

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

159 
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

160 
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) 
59081  161 
else if Token.is_kind Token.Alt_String tok then 
49320
94bd2fb83d11
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents:
48628
diff
changeset

162 
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

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

164 
let 
59809  165 
val ants = Antiquote.read (Token.input_of tok); 
27874
f0364f1c0ecf
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents:
27809
diff
changeset

166 
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

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

17081  170 
else output_syms s 
61404  171 
end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); 
17081  172 

61404  173 

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

175 

17081  176 
val begin_delim = enclose "%\n\\isadelim" "\n"; 
177 
val end_delim = enclose "%\n\\endisadelim" "\n"; 

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

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

11860  180 

181 

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

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

183 

61462  184 
fun environment name = 
61516
8e3705d91cfa
clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
wenzelm
parents:
61505
diff
changeset

185 
enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}"); 
61462  186 

9707  187 
val tex_trailer = 
188 
"%%% Local Variables:\n\ 

9135  189 
\%%% mode: latex\n\ 
190 
\%%% TeXmaster: \"root\"\n\ 

9144  191 
\%%% End:\n"; 
8192  192 

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

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

195 
\\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ 
61462  196 
"%\n\\end{isabellebody}%\n" ^ tex_trailer; 
9707  197 

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

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

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

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

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

202 

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

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

204 

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

205 

8460  206 
(* print mode *) 
207 

8965  208 
val latexN = "latex"; 
17218  209 
val modes = [latexN, Symbol.xsymbolsN]; 
8965  210 

8460  211 
fun latex_output str = 
212 
let val syms = Symbol.explode str 

64526
01920e390645
embedded latex has 0 length  imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents:
63936
diff
changeset

213 
in (output_symbols syms, length_symbols syms) end; 
19265  214 

23621  215 
fun latex_markup (s, _) = 
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset

216 
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

217 
then ("\\isacommand{", "}") 
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset

218 
else if s = Markup.keyword2N 
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59081
diff
changeset

219 
then ("\\isakeyword{", "}") 
29325  220 
else Markup.no_output; 
10955  221 

23621  222 
fun latex_indent "" _ = "" 
223 
 latex_indent s _ = enclose "\\isaindent{" "}" s; 

224 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63590
diff
changeset

225 
val _ = Output.add_mode latexN latex_output embed_raw; 
23703  226 
val _ = Markup.add_mode latexN latex_markup; 
227 
val _ = Pretty.add_mode latexN latex_indent; 

8460  228 

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

229 
end; 