author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 5229  7c8abffc4413 
child 5870  5d4fc952be47 
permissions  rwrr 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Syntax/symbol.ML 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

4 

4901  5 
Generalized characters. 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

6 
*) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

7 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

8 
signature SYMBOL = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

9 
sig 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

10 
type symbol 
4901  11 
val space: symbol 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

12 
val eof: symbol 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

13 
val is_eof: symbol > bool 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

14 
val not_eof: symbol > bool 
4938  15 
val stopper: symbol * (symbol > bool) 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

16 
val is_ascii: symbol > bool 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

17 
val is_letter: symbol > bool 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

18 
val is_digit: symbol > bool 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

19 
val is_quasi_letter: symbol > bool 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

20 
val is_letdig: symbol > bool 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

21 
val is_blank: symbol > bool 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

22 
val is_printable: symbol > bool 
5112  23 
val beginning: symbol list > string 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

24 
val scan: string list > symbol * string list 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

25 
val explode: string > symbol list 
5229  26 
val length: symbol list > int 
27 
val size: string > int 

4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

28 
val input: string > string 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

29 
val output: string > string 
4959  30 
val source: bool > (string, 'a) Source.source > 
31 
(symbol, (string, 'a) Source.source) Source.source 

4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

32 
end; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

33 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

34 
structure Symbol: SYMBOL = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

35 
struct 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

36 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

37 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

38 
(** encoding table (isabelle0) **) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

39 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

40 
val enc_start = 160; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

41 
val enc_end = 255; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

42 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

43 
val enc_vector = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

44 
[ 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

45 
(* GENERATED TEXT FOLLOWS  Do not edit! *) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

46 
"\\<space2>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

47 
"\\<Gamma>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

48 
"\\<Delta>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

49 
"\\<Theta>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

50 
"\\<Lambda>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

51 
"\\<Pi>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

52 
"\\<Sigma>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

53 
"\\<Phi>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

54 
"\\<Psi>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

55 
"\\<Omega>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

56 
"\\<alpha>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

57 
"\\<beta>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

58 
"\\<gamma>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

59 
"\\<delta>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

60 
"\\<epsilon>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

61 
"\\<zeta>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

62 
"\\<eta>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

63 
"\\<theta>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

64 
"\\<kappa>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

65 
"\\<lambda>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

66 
"\\<mu>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

67 
"\\<nu>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

68 
"\\<xi>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

69 
"\\<pi>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

70 
"\\<rho>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

71 
"\\<sigma>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

72 
"\\<tau>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

73 
"\\<phi>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

74 
"\\<chi>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

75 
"\\<psi>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

76 
"\\<omega>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

77 
"\\<not>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

78 
"\\<and>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

79 
"\\<or>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

80 
"\\<forall>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

81 
"\\<exists>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

82 
"\\<And>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

83 
"\\<lceil>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

84 
"\\<rceil>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

85 
"\\<lfloor>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

86 
"\\<rfloor>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

87 
"\\<turnstile>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

88 
"\\<Turnstile>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

89 
"\\<lbrakk>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

90 
"\\<rbrakk>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

91 
"\\<cdot>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

92 
"\\<in>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

93 
"\\<subseteq>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

94 
"\\<inter>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

95 
"\\<union>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

96 
"\\<Inter>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

97 
"\\<Union>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

98 
"\\<sqinter>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

99 
"\\<squnion>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

100 
"\\<Sqinter>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

101 
"\\<Squnion>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

102 
"\\<bottom>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

103 
"\\<doteq>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

104 
"\\<equiv>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

105 
"\\<noteq>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

106 
"\\<sqsubset>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

107 
"\\<sqsubseteq>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

108 
"\\<prec>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

109 
"\\<preceq>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

110 
"\\<succ>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

111 
"\\<approx>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

112 
"\\<sim>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

113 
"\\<simeq>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

114 
"\\<le>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

115 
"\\<Colon>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

116 
"\\<leftarrow>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

117 
"\\<midarrow>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

118 
"\\<rightarrow>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

119 
"\\<Leftarrow>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

120 
"\\<Midarrow>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

121 
"\\<Rightarrow>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

122 
"\\<bow>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

123 
"\\<mapsto>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

124 
"\\<leadsto>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

125 
"\\<up>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

126 
"\\<down>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

127 
"\\<notin>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

128 
"\\<times>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

129 
"\\<oplus>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

130 
"\\<ominus>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

131 
"\\<otimes>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

132 
"\\<oslash>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

133 
"\\<subset>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

134 
"\\<infinity>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

135 
"\\<box>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

136 
"\\<diamond>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

137 
"\\<circ>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

138 
"\\<bullet>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

139 
"\\<parallel>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

140 
"\\<surd>", 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

141 
"\\<copyright>" 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

142 
(* END OF GENERATED TEXT *) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

143 
]; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

144 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

145 
val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end); 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

146 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

147 
val char_tab = Symtab.make enc_rel; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

148 
val symbol_tab = Symtab.make (map swap enc_rel); 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

149 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

150 
fun lookup_symbol c = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

151 
if ord c < enc_start then None 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

152 
else Symtab.lookup (symbol_tab, c); 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

153 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

154 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

155 
(* encode / decode *) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

156 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

157 
fun char s = if_none (Symtab.lookup (char_tab, s)) s; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

158 
fun symbol c = if_none (lookup_symbol c) c; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

159 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

160 
fun symbol' c = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

161 
(case lookup_symbol c of 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

162 
None => c 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

163 
 Some s => "\\" ^ s); 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

164 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

165 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

166 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

167 
(** type symbol **) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

168 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

169 
type symbol = string; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

170 

4901  171 
val space = " "; 
172 
val eof = ""; 

173 

4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

174 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

175 
(* kinds *) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

176 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

177 
fun is_eof s = s = eof; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

178 
fun not_eof s = s <> eof; 
4938  179 
val stopper = (eof, is_eof); 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

180 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

181 
fun is_ascii s = size s = 1 andalso ord s < 128; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

182 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

183 
fun is_letter s = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

184 
size s = 1 andalso 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

185 
(ord "A" <= ord s andalso ord s <= ord "Z" orelse 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

186 
ord "a" <= ord s andalso ord s <= ord "z"); 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

187 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

188 
fun is_digit s = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

189 
size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

190 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

191 
fun is_quasi_letter "_" = true 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

192 
 is_quasi_letter "'" = true 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

193 
 is_quasi_letter s = is_letter s; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

194 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

195 
val is_blank = 
4715  196 
fn " " => true  "\t" => true  "\n" => true  "\^L" => true 
197 
 "\160" => true  "\\<space2>" => true 

4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

198 
 _ => false; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

199 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

200 
val is_letdig = is_quasi_letter orf is_digit; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

201 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

202 
fun is_printable s = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

203 
size s = 1 andalso ord " " <= ord s andalso ord s <= ord "~" orelse 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

204 
size s > 2 andalso nth_elem (2, explode s) <> "^"; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

205 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

206 

5112  207 
(* beginning *) 
208 

209 
val smash_blanks = map (fn s => if is_blank s then space else s); 

210 

211 
fun beginning raw_ss = 

212 
let 

213 
val (all_ss, _) = take_suffix is_blank raw_ss; 

214 
val dots = if length all_ss > 10 then " ..." else ""; 

215 
val (ss, _) = take_suffix is_blank (take (10, all_ss)); 

216 
in implode (smash_blanks ss) ^ dots end; 

217 

218 

4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

219 
(* scan *) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

220 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

221 
val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode); 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

222 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

223 
val scan = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

224 
($$ "\\"  Scan.optional ($$ "\\") "") ^^ $$ "<" ^^ 
4921  225 
!! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs) 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

226 
(Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">")  
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

227 
Scan.one not_eof; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

228 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

229 

4959  230 
(* source *) 
231 

232 
val recover = Scan.any1 ((not o is_blank) andf not_eof); 

233 

234 
fun source do_recover src = 

235 
Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src; 

236 

237 

4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

238 
(* explode *) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

239 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

240 
fun no_syms [] = true 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

241 
 no_syms ("\\" :: "<" :: _) = false 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

242 
 no_syms (c :: cs) = ord c < enc_start andalso no_syms cs; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

243 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

244 
fun sym_explode str = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

245 
let val chs = explode str in 
4901  246 
if no_syms chs then chs (*tune trivial case*) 
4938  247 
else map symbol (#1 (Scan.error (Scan.finite stopper (Scan.repeat scan)) chs)) 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

248 
end; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

249 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

250 

5229  251 
(* printable length *) 
252 

253 
fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss); 

254 
val sym_size = sym_length o sym_explode; 

255 

256 

4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

257 
(* input / output *) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

258 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

259 
fun input str = 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

260 
let val chs = explode str in 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

261 
if forall (fn c => ord c < enc_start) chs then str 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

262 
else implode (map symbol' chs) 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

263 
end; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

264 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

265 
val output = implode o map char o sym_explode; 
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

266 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

267 

5229  268 
(*final declarations of this structure!*) 
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

269 
val explode = sym_explode; 
5229  270 
val length = sym_length; 
271 
val size = sym_size; 

4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

272 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

273 

8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset

274 
end; 