author  wenzelm 
Thu, 21 Apr 2005 22:02:06 +0200  
changeset 15801  d2f5ca3c048d 
parent 14992  a16bc5abad45 
child 17081  e19963723262 
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 
ID: $Id$ 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

4 

15801  5 
LaTeX presentation elements  based on outer lexical syntax. 
7726
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 

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

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

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

11719  12 
val output_symbols: Symbol.symbol list > string 
9135  13 
datatype token = Basic of OuterLex.token  Markup of string  MarkupEnv of string  Verbatim 
14 
val output_tokens: (token * string) list > string 

11860  15 
val flag_markup: bool > string 
9707  16 
val tex_trailer: string 
9916  17 
val isabelle_file: string > string > string 
14924  18 
val symbol_source: (string > bool) * (string > bool) > 
19 
string > Symbol.symbol list > string 

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

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

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

23 

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

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

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

26 

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

27 

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

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

29 

7900  30 
local 
31 

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

32 
val output_chr = fn 
9505  33 
" " => "\\ "  
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

34 
"\n" => "\\isanewline\n"  
9668  35 
"!" => "{\\isacharbang}"  
36 
"\"" => "{\\isachardoublequote}"  

9663  37 
"#" => "{\\isacharhash}"  
38 
"$" => "{\\isachardollar}"  

39 
"%" => "{\\isacharpercent}"  

40 
"&" => "{\\isacharampersand}"  

41 
"'" => "{\\isacharprime}"  

42 
"(" => "{\\isacharparenleft}"  

43 
")" => "{\\isacharparenright}"  

44 
"*" => "{\\isacharasterisk}"  

9668  45 
"+" => "{\\isacharplus}"  
46 
"," => "{\\isacharcomma}"  

9663  47 
"" => "{\\isacharminus}"  
9668  48 
"." => "{\\isachardot}"  
49 
"/" => "{\\isacharslash}"  

50 
":" => "{\\isacharcolon}"  

51 
";" => "{\\isacharsemicolon}"  

9663  52 
"<" => "{\\isacharless}"  
9668  53 
"=" => "{\\isacharequal}"  
9663  54 
">" => "{\\isachargreater}"  
9668  55 
"?" => "{\\isacharquery}"  
56 
"@" => "{\\isacharat}"  

9663  57 
"[" => "{\\isacharbrackleft}"  
58 
"\\" => "{\\isacharbackslash}"  

59 
"]" => "{\\isacharbrackright}"  

60 
"^" => "{\\isacharcircum}"  

61 
"_" => "{\\isacharunderscore}"  

9668  62 
"`" => "{\\isacharbackquote}"  
9663  63 
"{" => "{\\isacharbraceleft}"  
64 
"" => "{\\isacharbar}"  

65 
"}" => "{\\isacharbraceright}"  

66 
"~" => "{\\isachartilde}"  

14992  67 
c => 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

68 

14924  69 
val output_chrs = translate_string output_chr; 
70 

71 
fun output_known_sym (known_sym, known_ctrl) sym = 

14874  72 
(case Symbol.decode sym of 
73 
Symbol.Char s => output_chr s 

14924  74 
 Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym 
75 
 Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym 

14874  76 
 Symbol.Raw s => s); 
7900  77 

78 
in 

79 

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

8192  82 
val output_syms = output_symbols o Symbol.explode; 
7900  83 

84 
end; 

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

85 

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

86 

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

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

88 

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

89 
structure T = OuterLex; 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

90 

8660  91 
datatype token = 
92 
Basic of T.token  

9135  93 
Markup of string  
94 
MarkupEnv of string  

95 
Verbatim; 

7756  96 

97 

98 
val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment; 

99 

9135  100 
fun output_tok (Basic tok, _) = 
7752  101 
let val s = T.val_of tok in 
7756  102 
if invisible_token tok then "" 
7800  103 
else if T.is_kind T.Command tok then 
9668  104 
"\\isacommand{" ^ output_syms s ^ "}" 
14680  105 
else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then 
7900  106 
"\\isakeyword{" ^ output_syms s ^ "}" 
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14561
diff
changeset

107 
else if T.is_kind T.String tok then output_syms (Library.quote s) 
7900  108 
else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s) 
109 
else output_syms s 

7756  110 
end 
11012  111 
 output_tok (Markup cmd, txt) = 
112 
"%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n" 

9135  113 
 output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ 
11012  114 
Symbol.strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n" 
115 
 output_tok (Verbatim, txt) = "%\n" ^ Symbol.strip_blanks txt ^ "\n"; 

7745  116 

7756  117 

118 
val output_tokens = implode o map output_tok; 

7726
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 

11860  121 
fun flag_markup true = "\\isamarkuptrue%\n" 
122 
 flag_markup false = "\\isamarkupfalse%\n"; 

123 

124 

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

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

126 

9707  127 
val tex_trailer = 
128 
"%%% Local Variables:\n\ 

9135  129 
\%%% mode: latex\n\ 
130 
\%%% TeXmaster: \"root\"\n\ 

9144  131 
\%%% End:\n"; 
8192  132 

9916  133 
fun isabelle_file name txt = 
134 
"%\n\\begin{isabellebody}%\n\ 

10247  135 
\\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ 
9916  136 
"\\end{isabellebody}%\n" ^ tex_trailer; 
9707  137 

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

140 
output_known_symbols known syms); 

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

141 

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

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

143 

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

144 

8460  145 
(* print mode *) 
146 

8965  147 
val latexN = "latex"; 
9135  148 
val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN]; 
8965  149 

8460  150 
fun latex_output str = 
151 
let val syms = Symbol.explode str 

152 
in (output_symbols syms, real (Symbol.length syms)) end; 

153 

10955  154 
fun latex_indent "" = "" 
155 
 latex_indent s = enclose "\\isaindent{" "}" s; 

156 

14973  157 
val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.encode_raw); 
8460  158 

159 

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

160 
end; 