author  berghofe 
Wed, 10 Oct 2001 18:41:13 +0200  
changeset 11719  49c14348a42b 
parent 11012  8eb472444705 
child 11860  36ba0d4a836c 
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 
11719  11 
val output_symbols: Symbol.symbol list > string 
9135  12 
datatype token = Basic of OuterLex.token  Markup of string  MarkupEnv of string  Verbatim 
13 
val output_tokens: (token * string) list > string 

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

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

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

21 

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

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

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

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

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

27 

7900  28 
local 
29 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

63 
"}" => "{\\isacharbraceright}"  

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

10184  65 
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

66 

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

69 
else 

70 
(case explode s of 

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

75 
in 

76 

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

7900  79 

80 
end; 

7726
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 

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

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

84 

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

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

86 

8660  87 
datatype token = 
88 
Basic of T.token  

9135  89 
Markup of string  
90 
MarkupEnv of string  

91 
Verbatim; 

7756  92 

93 

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

95 

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

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

105 
else output_syms s 

7756  106 
end 
11012  107 
 output_tok (Markup cmd, txt) = 
108 
"%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n" 

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

7745  112 

7756  113 

114 
val output_tokens = implode o map output_tok; 

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

115 

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

116 

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

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

118 

9707  119 
val tex_trailer = 
120 
"%%% Local Variables:\n\ 

9135  121 
\%%% mode: latex\n\ 
122 
\%%% TeXmaster: \"root\"\n\ 

9144  123 
\%%% End:\n"; 
8192  124 

9916  125 
fun isabelle_file name txt = 
126 
"%\n\\begin{isabellebody}%\n\ 

10247  127 
\\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ 
9916  128 
"\\end{isabellebody}%\n" ^ tex_trailer; 
9707  129 

8499  130 
fun old_symbol_source name syms = 
9916  131 
isabelle_file name ("\\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 

10955  145 
fun latex_indent "" = "" 
146 
 latex_indent s = enclose "\\isaindent{" "}" s; 

147 

9558  148 
val token_translation = 
9749
36ddd544a18d
token trans: removed \mbox to achieve proper italic correction;
wenzelm
parents:
9707
diff
changeset

149 
map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes; 
8965  150 

10955  151 
val _ = Symbol.add_mode latexN (latex_output, latex_indent o #1); 
8965  152 
val setup = [Theory.add_tokentrfuns token_translation]; 
8460  153 

154 

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

155 
end; 