# HG changeset patch
# User wenzelm
# Date 1353958759 -3600
# Node ID 476a3350589c28471f46387b23999d72ba497208
# Parent  b89b57bf4cf2defd14b545ce85dfb80adab2de2e
clarified Symbol.scan_ascii_id;
ATP: follow change from Symbol.scan_id to Symbol.scan_ascii_id, assuming that this was meant here, not fully symbolic Isabelle identifiers;

diff -r b89b57bf4cf2 -r 476a3350589c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Nov 26 20:29:40 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Nov 26 20:39:19 2012 +0100
@@ -390,7 +390,7 @@
 fun parse_tstp_line problem =
   ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
     || Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(")
-    |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
+    |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
     -- (parse_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments
     --| $$ ")" --| $$ "."
    >> (fn (((num, role), phi), deps) =>
@@ -469,7 +469,7 @@
            derived from formulae <ident>* *)
 fun parse_spass_line x =
   (parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
-     -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
+     -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]"
      -- parse_horn_clause --| $$ "."
      -- Scan.option (Scan.this_string "derived from formulae "
                      |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
diff -r b89b57bf4cf2 -r 476a3350589c src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Nov 26 20:29:40 2012 +0100
+++ b/src/Pure/General/symbol.ML	Mon Nov 26 20:39:19 2012 +0100
@@ -30,10 +30,12 @@
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
   val is_ascii_control: symbol -> bool
+  val is_ascii_letdig: symbol -> bool
   val is_ascii_lower: symbol -> bool
   val is_ascii_upper: symbol -> bool
   val to_ascii_lower: symbol -> symbol
   val to_ascii_upper: symbol -> symbol
+  val scan_ascii_id: string list -> string * string list
   val is_raw: symbol -> bool
   val decode_raw: symbol -> string
   val encode_raw: string -> string
@@ -53,7 +55,6 @@
   val is_ident: symbol list -> bool
   val beginning: int -> symbol list -> string
   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
-  val scan_id: string list -> string * string list
   val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
   val split_words: symbol list -> string list
@@ -152,12 +153,16 @@
 
 fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
 
+fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s;
+
 fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");
 fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");
 
 fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + ord "a" - ord "A") else s;
 fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + ord "A" - ord "a") else s;
 
+val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode);
+
 
 (* encode_raw *)
 
@@ -414,8 +419,6 @@
     | (_, rest) => error (message (rest, NONE) ()))
   end;
 
-val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);
-
 
 (* source *)
 
@@ -443,7 +446,7 @@
   Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
   scan_encoded_newline ||
   ($$ "\\" ^^ $$ "<" ^^
-    (($$ "^" ^^ Scan.optional (scan_raw || scan_id) "" || Scan.optional scan_id "") ^^
+    (($$ "^" ^^ Scan.optional (scan_raw || scan_ascii_id) "" || Scan.optional scan_ascii_id "") ^^
       Scan.optional ($$ ">") "")) ||
   Scan.one not_eof;