Removed the extended digits again.
authorskalberg
Fri Aug 29 13:18:45 2003 +0200 (2003-08-29)
changeset 14173a3690aeb79d4
parent 14172 a872d646bf01
child 14174 f3cafd2929d5
Removed the extended digits again.
NEWS
src/Pure/General/symbol.ML
     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 =