# HG changeset patch # User wenzelm # Date 950212379 -3600 # Node ID 6f8aa407bcf9ba6139ffa0703e2de08a671a908e # Parent 38f453607c61d4dc02f2d1ccc3688dbbacc6e448 is_symbolic; diff -r 38f453607c61 -r 6f8aa407bcf9 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Thu Feb 10 13:36:23 2000 +0100 +++ b/src/Pure/General/symbol.ML Thu Feb 10 20:52:59 2000 +0100 @@ -22,6 +22,7 @@ val is_quasi_letter: symbol -> bool val is_letdig: symbol -> bool val is_blank: symbol -> bool + val is_symbolic: symbol -> bool val is_printable: symbol -> bool val length: symbol list -> int val beginning: symbol list -> string @@ -92,9 +93,13 @@ val is_letdig = is_quasi_letter orf is_digit; +fun is_symbolic s = + size s > 2 andalso nth_elem_string (2, s) <> "^"; + fun is_printable s = size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse - size s > 2 andalso nth_elem_string (2, s) <> "^"; + is_symbolic s; + fun sym_length ss = foldl (fn (n, s) => if is_printable s then n + 1 else n) (0, ss);