author  wenzelm 
Mon, 28 Aug 2000 20:32:55 +0200  
changeset 9707  067c25edd1bd 
parent 9668  b5e709fd1e42 
child 9749  36ddd544a18d 
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 
8808  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

5 

8460  6 
LaTeX presentation primitives (based on outer lexical syntax). 
7726
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 

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

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

10 
sig 
9135  11 
datatype token = Basic of OuterLex.token  Markup of string  MarkupEnv of string  Verbatim 
12 
val output_tokens: (token * string) list > string 

9707  13 
val tex_trailer: string 
9135  14 
val isabelle_file: string > string 
8499  15 
val old_symbol_source: string > Symbol.symbol list > string 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

16 
val theory_entry: string > string 
9135  17 
val modes: string list 
8965  18 
val setup: (theory > theory) list 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

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

20 

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

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

22 
struct 
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 

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

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

26 

7900  27 
local 
28 

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

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

31 
"\n" => "\\isanewline\n"  
9668  32 
"!" => "{\\isacharbang}"  
33 
"\"" => "{\\isachardoublequote}"  

9663  34 
"#" => "{\\isacharhash}"  
35 
"$" => "{\\isachardollar}"  

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

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

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

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

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

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

9668  42 
"+" => "{\\isacharplus}"  
43 
"," => "{\\isacharcomma}"  

9663  44 
"" => "{\\isacharminus}"  
9668  45 
"." => "{\\isachardot}"  
46 
"/" => "{\\isacharslash}"  

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

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

9663  49 
"<" => "{\\isacharless}"  
9668  50 
"=" => "{\\isacharequal}"  
9663  51 
">" => "{\\isachargreater}"  
9668  52 
"?" => "{\\isacharquery}"  
53 
"@" => "{\\isacharat}"  

9663  54 
"[" => "{\\isacharbrackleft}"  
55 
"\\" => "{\\isacharbackslash}"  

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

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

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

9668  59 
"`" => "{\\isacharbackquote}"  
9663  60 
"{" => "{\\isacharbraceleft}"  
61 
"" => "{\\isacharbar}"  

62 
"}" => "{\\isacharbraceright}"  

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

9668  64 
c => if Symbol.is_digit c then enclose "\\isadigit{" "}" c else c; 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

65 

7900  66 
fun output_sym s = 
67 
if size s = 1 then output_chr s 

68 
else 

69 
(case explode s of 

70 
cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs) 

7973  71 
 "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}" 
7900  72 
 _ => sys_error "output_sym"); 
73 

74 
in 

75 

8192  76 
val output_symbols = implode o map output_sym; 
77 
val output_syms = output_symbols o Symbol.explode; 

7900  78 

79 
end; 

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

80 

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

81 

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

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

83 

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

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

85 

8660  86 
datatype token = 
87 
Basic of T.token  

9135  88 
Markup of string  
89 
MarkupEnv of string  

90 
Verbatim; 

7756  91 

92 

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

94 

95 
fun strip_blanks s = 

96 
implode (#1 (Library.take_suffix Symbol.is_blank 

97 
(#2 (Library.take_prefix Symbol.is_blank (explode s))))); 

98 

9135  99 
fun output_tok (Basic tok, _) = 
7752  100 
let val s = T.val_of tok in 
7756  101 
if invisible_token tok then "" 
7800  102 
else if T.is_kind T.Command tok then 
9668  103 
"\\isacommand{" ^ output_syms s ^ "}" 
7800  104 
else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then 
7900  105 
"\\isakeyword{" ^ output_syms s ^ "}" 
106 
else if T.is_kind T.String tok then output_syms (quote s) 

107 
else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s) 

108 
else output_syms s 

7756  109 
end 
9135  110 
 output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n" 
111 
 output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ 

8660  112 
strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n" 
9135  113 
 output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n"; 
7745  114 

7756  115 

116 
val output_tokens = implode o map output_tok; 

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

117 

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 
(* theory presentation *) 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

120 

9707  121 
val tex_trailer = 
122 
"%%% Local Variables:\n\ 

9135  123 
\%%% mode: latex\n\ 
124 
\%%% TeXmaster: \"root\"\n\ 

9144  125 
\%%% End:\n"; 
8192  126 

9707  127 
val isabelle_file = 
128 
enclose "%\n\\begin{isabellebody}%\n" ("\\end{isabellebody}%\n" ^ tex_trailer); 

129 

8499  130 
fun old_symbol_source name syms = 
9135  131 
isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms); 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

132 

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

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

134 

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

135 

8460  136 
(* print mode *) 
137 

8965  138 
val latexN = "latex"; 
9135  139 
val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN]; 
8965  140 

8460  141 
fun latex_output str = 
142 
let val syms = Symbol.explode str 

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

144 

9558  145 
val token_translation = 
146 
map (fn s => (latexN, s, apfst (enclose "\\mbox{" "}") o latex_output)) 

147 
Syntax.standard_token_classes; 

8965  148 

149 
val _ = Symbol.add_mode latexN latex_output; 

150 
val setup = [Theory.add_tokentrfuns token_translation]; 

8460  151 

152 

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

153 
end; 