summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | skalberg |

Fri, 29 Aug 2003 13:18:45 +0200 | |

changeset 14173 | a3690aeb79d4 |

parent 14172 | a872d646bf01 |

child 14174 | f3cafd2929d5 |

Removed the extended digits again.

NEWS | file | annotate | diff | comparison | revisions | |

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

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

--- a/src/Pure/General/symbol.ML Thu Aug 28 02:00:16 2003 +0200 +++ b/src/Pure/General/symbol.ML Fri Aug 29 13:18:45 2003 +0200 @@ -87,9 +87,6 @@ local fun wrap s = "\\<" ^ s ^ ">" - val pre_digits = - ["zero","one","two","three","four", - "five","six","seven","eight","nine"] val cal_letters = ["A","B","C","D","E","F","G","H","I","J","K","L","M", @@ -119,12 +116,9 @@ goth_letters @ greek_letters in -val ext_digits = map wrap pre_digits val ext_letters = map wrap pre_letters -val ext_letdigs = ext_digits @ ext_letters -fun is_ext_digit s = String.isPrefix "\\<" s andalso s mem ext_digits + fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters -fun is_ext_letdig s = String.isPrefix "\\<" s andalso s mem ext_letdigs end fun is_letter s = @@ -134,8 +128,7 @@ orelse is_ext_letter s fun is_digit s = - (size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9") - orelse is_ext_digit s + size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9" fun is_quasi "_" = true | is_quasi "'" = true @@ -152,11 +145,11 @@ fun is_symbolic s = size s > 2 andalso nth_elem_string (2, s) <> "^" - andalso not (is_ext_letdig s); + andalso not (is_ext_letter s); fun is_printable s = size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse - is_ext_letdig s orelse + is_ext_letter s orelse is_symbolic s; fun is_identifier s =