author  wenzelm 
Wed, 24 May 2000 19:09:36 +0200  
changeset 8965  d46b36785c70 
parent 8896  c80aba8c1d5e 
child 9038  63d20536971f 
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 
8660  11 
datatype token = Basic of OuterLex.token  Markup of string * string  
12 
MarkupEnv of string * string  Verbatim of string 

8499  13 
val old_symbol_source: string > Symbol.symbol list > string 
7756  14 
val token_source: token list > string 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

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

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

18 

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

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

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

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

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

24 

7900  25 
local 
26 

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

27 
val output_chr = fn 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

28 
" " => "~"  
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

29 
"\n" => "\\isanewline\n"  
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 
"&" => "\\&"  
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

32 
"%" => "\\%"  
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

33 
"#" => "\\#"  
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

34 
"_" => "\\_"  
7800  35 
"{" => "{\\isabraceleft}"  
36 
"}" => "{\\isabraceright}"  

37 
"~" => "{\\isatilde}"  

38 
"^" => "{\\isacircum}"  

7752  39 
"\"" => "{\"}"  
7800  40 
"\\" => "{\\isabackslash}"  
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

41 
c => c; 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

42 

7900  43 
fun output_sym s = 
44 
if size s = 1 then output_chr s 

45 
else 

46 
(case explode s of 

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

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

51 
in 

52 

8192  53 
val output_symbols = implode o map output_sym; 
54 
val output_syms = output_symbols o Symbol.explode; 

7900  55 

56 
end; 

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

57 

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

58 

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

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

60 

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

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

62 

8660  63 
datatype token = 
64 
Basic of T.token  

65 
Markup of string * string  

66 
MarkupEnv of string * string  

67 
Verbatim of string; 

7756  68 

69 

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

71 

72 
fun strip_blanks s = 

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

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

75 

76 
fun output_tok (Basic tok) = 

7752  77 
let val s = T.val_of tok in 
7756  78 
if invisible_token tok then "" 
7800  79 
else if T.is_kind T.Command tok then 
8896  80 
if s = "{" then "{\\isabeginblock}" 
81 
else if s = "}" then "{\\isaendblock}" 

7900  82 
else "\\isacommand{" ^ output_syms s ^ "}" 
7800  83 
else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then 
7900  84 
"\\isakeyword{" ^ output_syms s ^ "}" 
85 
else if T.is_kind T.String tok then output_syms (quote s) 

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

87 
else output_syms s 

7756  88 
end 
7852  89 
 output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n" 
8660  90 
 output_tok (MarkupEnv (cmd, txt)) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^ 
91 
strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n" 

7852  92 
 output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n"; 
7745  93 

7756  94 

95 
val output_tokens = implode o map output_tok; 

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

96 

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

97 

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

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

99 

8460  100 
val isabelle_env = enclose "\\begin{isabelle}%\n" "\\end{isabelle}%\n"; 
8192  101 

8499  102 
fun old_symbol_source name syms = 
103 
isabelle_env ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms); 

104 

8460  105 
val token_source = isabelle_env o output_tokens; 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

106 

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

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

108 

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

109 

8460  110 
(* print mode *) 
111 

8965  112 
val latexN = "latex"; 
113 

8460  114 
fun latex_output str = 
115 
let val syms = Symbol.explode str 

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

117 

8965  118 
val token_translation = map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes; 
119 

120 
val _ = Symbol.add_mode latexN latex_output; 

121 
val setup = [Theory.add_tokentrfuns token_translation]; 

8460  122 

123 

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

124 
end; 