author  wenzelm 
Thu, 21 Oct 1999 18:43:06 +0200  
changeset 7900  e62973fccc97 
parent 7852  d28dff7ac48d 
child 7973  0d801c6e4dc0 
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 
7756  11 
val token_source: token list > string 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

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

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

14 

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

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

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

17 

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

20 

7900  21 
local 
22 

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

23 
val output_chr = fn 
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 
"\n" => "\\isanewline\n"  
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 
"%" => "\\%"  
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 
"_" => "\\_"  
7800  31 
"{" => "{\\isabraceleft}"  
32 
"}" => "{\\isabraceright}"  

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

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

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

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

38 

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

41 
else 

42 
(case explode s of 

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

44 
 "\\" :: "<" :: cs => "{\\isasymbol" ^ implode (#1 (Library.split_last cs)) ^ "}" 

45 
 _ => sys_error "output_sym"); 

46 

47 
in 

48 

49 
val output_syms = implode o map output_sym o Symbol.explode; 

50 

51 
end; 

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

52 

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

53 

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

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

57 

7789  58 
datatype token = Basic of T.token  Markup of string * string  Verbatim of string; 
7756  59 

60 

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

62 

63 
fun strip_blanks s = 

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

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

66 

67 
fun output_tok (Basic tok) = 

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

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

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

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

78 
else output_syms s 

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

7745  82 

7756  83 

84 
val output_tokens = implode o map output_tok; 

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 
(* theory presentation *) 
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 
fun token_source toks = 
7756  90 
"\\begin{isabellesimple}\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n"; 
7726
2c7fc0ba1e12
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff
changeset

91 

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

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

93 

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

94 

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

95 
end; 