83 fun not_eof s = s <> eof; |
83 fun not_eof s = s <> eof; |
84 val stopper = (eof, is_eof); |
84 val stopper = (eof, is_eof); |
85 |
85 |
86 fun is_ascii s = size s = 1 andalso ord s < 128; |
86 fun is_ascii s = size s = 1 andalso ord s < 128; |
87 |
87 |
|
88 local |
|
89 fun wrap s = "\\<" ^ s ^ ">" |
|
90 val pre_digits = |
|
91 ["zero","one","two","three","four", |
|
92 "five","six","seven","eight","nine"] |
|
93 |
|
94 val cal_letters = |
|
95 ["A","B","C","D","E","F","G","H","I","J","K","L","M", |
|
96 "N","O","P","Q","R","S","T","U","V","W","X","Y","Z"] |
|
97 |
|
98 val small_letters = |
|
99 ["a","b","c","d","e","f","g","h","i","j","k","l","m", |
|
100 "n","o","p","q","r","s","t","u","v","w","x","y","z"] |
|
101 |
|
102 val goth_letters = |
|
103 ["AA","BB","CC","DD","EE","FF","GG","HH","II","JJ","KK","LL","MM", |
|
104 "NN","OO","PP","QQ","RR","SS","TT","UU","VV","WW","XX","YY","ZZ", |
|
105 "aa","bb","cc","dd","ee","ff","gg","hh","ii","jj","kk","ll","mm", |
|
106 "nn","oo","pp","qq","rr","ss","tt","uu","vv","ww","xx","yy","zz"] |
|
107 |
|
108 val greek_letters = |
|
109 ["alpha","beta","gamma","delta","epsilon","zeta","eta","theta", |
|
110 "iota","kappa",(*"lambda",*)"mu","nu","xi","pi","rho","sigma","tau", |
|
111 "upsilon","phi","psi","omega","Gamma","Delta","Theta","Lambda", |
|
112 "Xi","Pi","Sigma","Upsilon","Phi","Psi","Omega"] |
|
113 |
|
114 val bbb_letters = ["bool","complex","nat","rat","real","int"] |
|
115 |
|
116 val pre_letters = |
|
117 cal_letters @ |
|
118 small_letters @ |
|
119 goth_letters @ |
|
120 greek_letters |
|
121 in |
|
122 val ext_digits = map wrap pre_digits |
|
123 val ext_letters = map wrap pre_letters |
|
124 val ext_letdigs = ext_digits @ ext_letters |
|
125 fun is_ext_digit s = String.isPrefix "\\<" s andalso s mem ext_digits |
|
126 fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters |
|
127 fun is_ext_letdig s = String.isPrefix "\\<" s andalso s mem ext_letdigs |
|
128 end |
|
129 |
88 fun is_letter s = |
130 fun is_letter s = |
89 size s = 1 andalso |
131 (size s = 1 andalso |
90 (ord "A" <= ord s andalso ord s <= ord "Z" orelse |
132 (ord "A" <= ord s andalso ord s <= ord "Z" orelse |
91 ord "a" <= ord s andalso ord s <= ord "z"); |
133 ord "a" <= ord s andalso ord s <= ord "z")) |
|
134 orelse is_ext_letter s |
92 |
135 |
93 fun is_digit s = |
136 fun is_digit s = |
94 size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; |
137 (size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9") |
|
138 orelse is_ext_digit s |
95 |
139 |
96 fun is_quasi "_" = true |
140 fun is_quasi "_" = true |
97 | is_quasi "'" = true |
141 | is_quasi "'" = true |
98 | is_quasi _ = false; |
142 | is_quasi _ = false; |
99 |
143 |