author | skalberg |

Fri Aug 29 13:18:45 2003 +0200 (2003-08-29) | |

changeset 14173 | a3690aeb79d4 |

parent 14172 | a872d646bf01 |

child 14174 | f3cafd2929d5 |

Removed the extended digits again.

NEWS | file | annotate | diff | revisions | |

src/Pure/General/symbol.ML | file | annotate | diff | revisions |

1.1 --- a/NEWS Thu Aug 28 02:00:16 2003 +0200 1.2 +++ b/NEWS Fri Aug 29 13:18:45 2003 +0200 1.3 @@ -7,16 +7,15 @@ 1.4 *** General *** 1.5 1.6 * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic 1.7 - (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and 1.8 - euler (\<a>...\<z>), are now considered normal letters, and can 1.9 - therefore be used anywhere where an ASCII letter (a...zA...Z) has 1.10 - until now. Similarily, the symbol digits \<zero>...\<nine> are now 1.11 - considered normal digits. COMPATIBILITY: This obviously changes the 1.12 - parsing of some terms, especially where a symbol has been used as a 1.13 - binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x 1.14 - will be parsed as an identifier. Fix it by inserting a space around 1.15 - former symbols. Call 'isatool fixgreek' to try to fix parsing 1.16 - errors in existing theory and ML files. 1.17 + (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler 1.18 + (\<a>...\<z>), are now considered normal letters, and can therefore 1.19 + be used anywhere where an ASCII letter (a...zA...Z) has until 1.20 + now. COMPATIBILITY: This obviously changes the parsing of some 1.21 + terms, especially where a symbol has been used as a binder, say 1.22 + '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed 1.23 + as an identifier. Fix it by inserting a space around former 1.24 + symbols. Call 'isatool fixgreek' to try to fix parsing errors in 1.25 + existing theory and ML files. 1.26 1.27 *** HOL *** 1.28

2.1 --- a/src/Pure/General/symbol.ML Thu Aug 28 02:00:16 2003 +0200 2.2 +++ b/src/Pure/General/symbol.ML Fri Aug 29 13:18:45 2003 +0200 2.3 @@ -87,9 +87,6 @@ 2.4 2.5 local 2.6 fun wrap s = "\\<" ^ s ^ ">" 2.7 - val pre_digits = 2.8 - ["zero","one","two","three","four", 2.9 - "five","six","seven","eight","nine"] 2.10 2.11 val cal_letters = 2.12 ["A","B","C","D","E","F","G","H","I","J","K","L","M", 2.13 @@ -119,12 +116,9 @@ 2.14 goth_letters @ 2.15 greek_letters 2.16 in 2.17 -val ext_digits = map wrap pre_digits 2.18 val ext_letters = map wrap pre_letters 2.19 -val ext_letdigs = ext_digits @ ext_letters 2.20 -fun is_ext_digit s = String.isPrefix "\\<" s andalso s mem ext_digits 2.21 + 2.22 fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters 2.23 -fun is_ext_letdig s = String.isPrefix "\\<" s andalso s mem ext_letdigs 2.24 end 2.25 2.26 fun is_letter s = 2.27 @@ -134,8 +128,7 @@ 2.28 orelse is_ext_letter s 2.29 2.30 fun is_digit s = 2.31 - (size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9") 2.32 - orelse is_ext_digit s 2.33 + size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9" 2.34 2.35 fun is_quasi "_" = true 2.36 | is_quasi "'" = true 2.37 @@ -152,11 +145,11 @@ 2.38 2.39 fun is_symbolic s = 2.40 size s > 2 andalso nth_elem_string (2, s) <> "^" 2.41 - andalso not (is_ext_letdig s); 2.42 + andalso not (is_ext_letter s); 2.43 2.44 fun is_printable s = 2.45 size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse 2.46 - is_ext_letdig s orelse 2.47 + is_ext_letter s orelse 2.48 is_symbolic s; 2.49 2.50 fun is_identifier s =