Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
authorwenzelm
Wed Jul 11 17:47:45 2007 +0200 (2007-07-11)
changeset 2378475e6b9dd5336
parent 23783 e4d514f81d95
child 23785 ea7c2ee8a47a
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
src/HOL/Import/xml.ML
src/Pure/General/symbol.ML
src/Pure/General/url.ML
src/Pure/Isar/antiquote.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Tools/codegen_names.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/xml.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Import/xml.ML	Wed Jul 11 12:23:34 2007 +0200
     1.2 +++ b/src/HOL/Import/xml.ML	Wed Jul 11 17:47:45 2007 +0200
     1.3 @@ -108,26 +108,26 @@
     1.4  val scan_special = $$ "&" ^^ scan_id ^^ $$ ";" >> decode;
     1.5  
     1.6  val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
     1.7 -  (scan_special || Scan.one Symbol.not_eof)) >> implode;
     1.8 +  (scan_special || Scan.one Symbol.is_regular)) >> implode;
     1.9  
    1.10  val parse_cdata = Scan.this_string "<![CDATA[" |--
    1.11 -  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
    1.12 +  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
    1.13      implode) --| Scan.this_string "]]>";
    1.14  
    1.15  val parse_att =
    1.16      scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
    1.17      (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
    1.18 -    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
    1.19 +    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
    1.20  
    1.21  val parse_comment = Scan.this_string "<!--" --
    1.22 -  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
    1.23 +  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
    1.24    Scan.this_string "-->";
    1.25  
    1.26  val scan_comment_whspc = 
    1.27      (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
    1.28  
    1.29  val parse_pi = Scan.this_string "<?" |--
    1.30 -  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.not_eof)) --|
    1.31 +  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
    1.32    Scan.this_string "?>";
    1.33  
    1.34  fun parse_content xs =
    1.35 @@ -153,7 +153,7 @@
    1.36  val parse_document =
    1.37    Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
    1.38      (Scan.repeat (Scan.unless ($$ ">")
    1.39 -      (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
    1.40 +      (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
    1.41    parse_elem;
    1.42  
    1.43  fun tree_of_string s =
     2.1 --- a/src/Pure/General/symbol.ML	Wed Jul 11 12:23:34 2007 +0200
     2.2 +++ b/src/Pure/General/symbol.ML	Wed Jul 11 17:47:45 2007 +0200
     2.3 @@ -15,13 +15,12 @@
     2.4    val is_printable: symbol -> bool
     2.5    val eof: symbol
     2.6    val is_eof: symbol -> bool
     2.7 -  val not_eof: symbol -> bool
     2.8    val stopper: symbol * (symbol -> bool)
     2.9    val sync: symbol
    2.10    val is_sync: symbol -> bool
    2.11 -  val not_sync: symbol -> bool
    2.12    val malformed: symbol
    2.13    val end_malformed: symbol
    2.14 +  val is_regular: symbol -> bool
    2.15    val is_ascii: symbol -> bool
    2.16    val is_ascii_letter: symbol -> bool
    2.17    val is_hex_letter: symbol -> bool
    2.18 @@ -110,13 +109,13 @@
    2.19  
    2.20  val sync = "\\<^sync>";
    2.21  fun is_sync s = s = sync;
    2.22 -fun not_sync s = s <> sync;
    2.23  
    2.24  val malformed = "[[";
    2.25  val end_malformed = "]]";
    2.26 +fun malformed_msg s = "Malformed symbolic character: " ^ quote (Output.escape_malformed s);
    2.27  
    2.28 -fun malformed_msg s =
    2.29 -  "Malformed symbolic character: " ^ quote (Output.escape_malformed s);
    2.30 +fun is_regular s =
    2.31 +  not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
    2.32  
    2.33  
    2.34  (* ascii symbols *)
     3.1 --- a/src/Pure/General/url.ML	Wed Jul 11 12:23:34 2007 +0200
     3.2 +++ b/src/Pure/General/url.ML	Wed Jul 11 17:47:45 2007 +0200
     3.3 @@ -53,11 +53,11 @@
     3.4  local
     3.5  
     3.6  val scan_host =
     3.7 -  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
     3.8 +  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
     3.9    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    3.10  
    3.11 -val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
    3.12 -val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
    3.13 +val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
    3.14 +val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
    3.15  
    3.16  val scan_url =
    3.17    Scan.unless (Scan.this_string "file:" ||
     4.1 --- a/src/Pure/Isar/antiquote.ML	Wed Jul 11 12:23:34 2007 +0200
     4.2 +++ b/src/Pure/Isar/antiquote.ML	Wed Jul 11 17:47:45 2007 +0200
     4.3 @@ -39,7 +39,7 @@
     4.4  val scan_txt =
     4.5    T.scan_blank ||
     4.6    T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
     4.7 -  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));
     4.8 +  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.is_regular s));
     4.9  
    4.10  fun escape "\\" = "\\\\"
    4.11    | escape "\"" = "\\\""
    4.12 @@ -50,7 +50,7 @@
    4.13  val scan_ant =
    4.14    T.scan_blank ||
    4.15    T.scan_string >> quote_escape ||
    4.16 -  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.not_sync s andalso Symbol.not_eof s));
    4.17 +  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
    4.18  
    4.19  val scan_antiq =
    4.20    T.keep_line ($$ "@" -- $$ "{") |--
     5.1 --- a/src/Pure/Syntax/lexicon.ML	Wed Jul 11 12:23:34 2007 +0200
     5.2 +++ b/src/Pure/Syntax/lexicon.ML	Wed Jul 11 17:47:45 2007 +0200
     5.3 @@ -216,7 +216,7 @@
     5.4  
     5.5  val scan_chr =
     5.6    $$ "\\" |-- $$ "'" ||
     5.7 -  Scan.one (fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) ||
     5.8 +  Scan.one (fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) ||
     5.9    $$ "'" --| Scan.ahead (~$$ "'");
    5.10  
    5.11  val scan_str =
    5.12 @@ -238,7 +238,7 @@
    5.13    Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) ||
    5.14    Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) ||
    5.15    Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) ||
    5.16 -  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.not_eof s));
    5.17 +  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s));
    5.18  
    5.19  val scan_comment =
    5.20    $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
    5.21 @@ -335,7 +335,7 @@
    5.22    let
    5.23      val scan =
    5.24        $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
    5.25 -      Scan.many Symbol.not_eof >> (free o implode);
    5.26 +      Scan.many Symbol.is_regular >> (free o implode);
    5.27    in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
    5.28  
    5.29  
    5.30 @@ -413,7 +413,7 @@
    5.31  fun read_idents str =
    5.32    let
    5.33      val blanks = Scan.many Symbol.is_blank;
    5.34 -    val junk = Scan.many Symbol.not_eof;
    5.35 +    val junk = Scan.many Symbol.is_regular;
    5.36      val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
    5.37    in
    5.38      (case Scan.read Symbol.stopper idents (Symbol.explode str) of
     6.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Jul 11 12:23:34 2007 +0200
     6.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Jul 11 17:47:45 2007 +0200
     6.3 @@ -194,8 +194,8 @@
     6.4  val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
     6.5  
     6.6  val scan_delim_char =
     6.7 -  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
     6.8 -  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
     6.9 +  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
    6.10 +  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
    6.11  
    6.12  fun read_int ["0", "0"] = ~1
    6.13    | read_int cs = #1 (Library.read_int cs);
     7.1 --- a/src/Pure/Tools/codegen_names.ML	Wed Jul 11 12:23:34 2007 +0200
     7.2 +++ b/src/Pure/Tools/codegen_names.ML	Wed Jul 11 17:47:45 2007 +0200
     7.3 @@ -40,7 +40,7 @@
     7.4  fun purify_name upper_else_lower =
     7.5    let
     7.6      fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
     7.7 -    val is_junk = not o is_valid andf Symbol.not_eof;
     7.8 +    val is_junk = not o is_valid andf Symbol.is_regular;
     7.9      val junk = Scan.many is_junk;
    7.10      val scan_valids = Symbol.scanner "Malformed input"
    7.11        ((junk |--
    7.12 @@ -179,7 +179,7 @@
    7.13    explode
    7.14    (*should disappear as soon as hierarchical theory name spaces are available*)
    7.15    #> Symbol.scanner "Malformed name"
    7.16 -      (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
    7.17 +      (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
    7.18    #> implode
    7.19    #> NameSpace.explode
    7.20    #> map (purify_name true);
     8.1 --- a/src/Pure/Tools/codegen_serializer.ML	Wed Jul 11 12:23:34 2007 +0200
     8.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Wed Jul 11 17:47:45 2007 +0200
     8.3 @@ -139,7 +139,7 @@
     8.4  
     8.5  fun parse_mixfix prep_arg s =
     8.6    let
     8.7 -    val sym_any = Scan.one Symbol.not_eof;
     8.8 +    val sym_any = Scan.one Symbol.is_regular;
     8.9      val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
    8.10           ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
    8.11        || ($$ "_" >> K (Arg BR))
     9.1 --- a/src/Pure/Tools/xml.ML	Wed Jul 11 12:23:34 2007 +0200
     9.2 +++ b/src/Pure/Tools/xml.ML	Wed Jul 11 17:47:45 2007 +0200
     9.3 @@ -122,28 +122,28 @@
     9.4  val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
     9.5  
     9.6  val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
     9.7 -  (scan_special || Scan.one Symbol.not_eof)) >> implode;
     9.8 +  (scan_special || Scan.one Symbol.is_regular)) >> implode;
     9.9  
    9.10  val parse_string = Scan.read Symbol.stopper parse_chars o explode;
    9.11  
    9.12  val parse_cdata = Scan.this_string "<![CDATA[" |--
    9.13 -  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
    9.14 +  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
    9.15      implode) --| Scan.this_string "]]>";
    9.16  
    9.17  val parse_att =
    9.18    Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
    9.19    (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
    9.20 -    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
    9.21 +    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
    9.22  
    9.23  val parse_comment = Scan.this_string "<!--" --
    9.24 -  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
    9.25 +  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
    9.26    Scan.this_string "-->";
    9.27  
    9.28  val scan_comment_whspc =
    9.29    (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
    9.30  
    9.31  val parse_pi = Scan.this_string "<?" |--
    9.32 -  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.not_eof)) --|
    9.33 +  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
    9.34    Scan.this_string "?>";
    9.35  
    9.36  fun parse_content xs =
    9.37 @@ -169,7 +169,7 @@
    9.38  val parse_document =
    9.39    Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
    9.40      (Scan.repeat (Scan.unless ($$ ">")
    9.41 -      (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
    9.42 +      (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
    9.43    parse_elem;
    9.44  
    9.45  fun tree_of_string s =
    10.1 --- a/src/Pure/codegen.ML	Wed Jul 11 12:23:34 2007 +0200
    10.2 +++ b/src/Pure/codegen.ML	Wed Jul 11 17:47:45 2007 +0200
    10.3 @@ -1087,13 +1087,13 @@
    10.4        || $$ "\\<module>" >> K Module
    10.5        || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
    10.6        || $$ "{" |-- $$ "*" |-- Scan.repeat1
    10.7 -           (   $$ "'" |-- Scan.one Symbol.not_eof
    10.8 -            || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
    10.9 +           (   $$ "'" |-- Scan.one Symbol.is_regular
   10.10 +            || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.is_regular)) --|
   10.11           $$ "*" --| $$ "}" >> (Quote o rd o implode)
   10.12        || Scan.repeat1
   10.13 -           (   $$ "'" |-- Scan.one Symbol.not_eof
   10.14 +           (   $$ "'" |-- Scan.one Symbol.is_regular
   10.15              || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
   10.16 -                 (Scan.one Symbol.not_eof)) >> (Pretty o str o implode)))
   10.17 +                 (Scan.one Symbol.is_regular)) >> (Pretty o str o implode)))
   10.18         (Symbol.explode s) of
   10.19       (p, []) => p
   10.20     | _ => error ("Malformed annotation: " ^ quote s));