author  wenzelm 
Fri, 04 Feb 2000 21:44:38 +0100  
changeset 8192  45a7027136e3 
parent 8117  0a6173c9b2d0 
child 8460  274426d1adbc 
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 

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

5 
Simple LaTeX presentation primitives (based on outer lexical syntax). 
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 
7789  10 
datatype token = Basic of OuterLex.token  Markup of string * string  Verbatim of string 
8192  11 
val old_symbol_source: Symbol.symbol list > string 
7756  12 
val token_source: token list > string 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

13 
val theory_entry: string > string 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

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

15 

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

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

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

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

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

21 

7900  22 
local 
23 

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

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

31 
"_" => "\\_"  
7800  32 
"{" => "{\\isabraceleft}"  
33 
"}" => "{\\isabraceright}"  

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

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

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

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

39 

7900  40 
fun output_sym s = 
41 
if size s = 1 then output_chr s 

42 
else 

43 
(case explode s of 

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

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

48 
in 

49 

8192  50 
val output_symbols = implode o map output_sym; 
51 
val output_syms = output_symbols o Symbol.explode; 

7900  52 

53 
end; 

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

54 

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

55 

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

56 
(* token output *) 
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 
structure T = OuterLex; 
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

59 

7789  60 
datatype token = Basic of T.token  Markup of string * string  Verbatim of string; 
7756  61 

62 

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

64 

65 
fun strip_blanks s = 

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

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

68 

69 
fun output_tok (Basic tok) = 

7752  70 
let val s = T.val_of tok in 
7756  71 
if invisible_token tok then "" 
7800  72 
else if T.is_kind T.Command tok then 
73 
if s = "{{" then "{\\isabeginblock}" 

74 
else if s = "}}" then "{\\isaendblock}" 

7900  75 
else "\\isacommand{" ^ output_syms s ^ "}" 
7800  76 
else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then 
7900  77 
"\\isakeyword{" ^ output_syms s ^ "}" 
78 
else if T.is_kind T.String tok then output_syms (quote s) 

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

80 
else output_syms s 

7756  81 
end 
7852  82 
 output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n" 
83 
 output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n"; 

7745  84 

7756  85 

86 
val output_tokens = implode o map output_tok; 

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

87 

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

90 

8192  91 
val isabelle_simple = enclose "\\begin{isabellesimple}%\n" "\\end{isabellesimple}%\n"; 
92 

93 
val old_symbol_source = isabelle_simple o output_symbols; 

94 
val token_source = isabelle_simple o output_tokens; 

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

95 

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

96 
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n"; 
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 

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

99 
end; 