Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
authorwenzelm
Wed, 11 Jul 2007 17:47:45 +0200
changeset 23784 75e6b9dd5336
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 file | annotate | diff | comparison | revisions
src/Pure/General/symbol.ML file | annotate | diff | comparison | revisions
src/Pure/General/url.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/antiquote.ML file | annotate | diff | comparison | revisions
src/Pure/Syntax/lexicon.ML file | annotate | diff | comparison | revisions
src/Pure/Syntax/syn_ext.ML file | annotate | diff | comparison | revisions
src/Pure/Tools/codegen_names.ML file | annotate | diff | comparison | revisions
src/Pure/Tools/codegen_serializer.ML file | annotate | diff | comparison | revisions
src/Pure/Tools/xml.ML file | annotate | diff | comparison | revisions
src/Pure/codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/xml.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/HOL/Import/xml.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -108,26 +108,26 @@
 val scan_special = $$ "&" ^^ scan_id ^^ $$ ";" >> decode;
 
 val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
-  (scan_special || Scan.one Symbol.not_eof)) >> implode;
+  (scan_special || Scan.one Symbol.is_regular)) >> implode;
 
 val parse_cdata = Scan.this_string "<![CDATA[" |--
-  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
+  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
     implode) --| Scan.this_string "]]>";
 
 val parse_att =
     scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
     (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
-    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
+    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
 
 val parse_comment = Scan.this_string "<!--" --
-  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
+  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
   Scan.this_string "-->";
 
 val scan_comment_whspc = 
     (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
 
 val parse_pi = Scan.this_string "<?" |--
-  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.not_eof)) --|
+  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
   Scan.this_string "?>";
 
 fun parse_content xs =
@@ -153,7 +153,7 @@
 val parse_document =
   Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
     (Scan.repeat (Scan.unless ($$ ">")
-      (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
+      (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
   parse_elem;
 
 fun tree_of_string s =
--- a/src/Pure/General/symbol.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/General/symbol.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -15,13 +15,12 @@
   val is_printable: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
-  val not_eof: symbol -> bool
   val stopper: symbol * (symbol -> bool)
   val sync: symbol
   val is_sync: symbol -> bool
-  val not_sync: symbol -> bool
   val malformed: symbol
   val end_malformed: symbol
+  val is_regular: symbol -> bool
   val is_ascii: symbol -> bool
   val is_ascii_letter: symbol -> bool
   val is_hex_letter: symbol -> bool
@@ -110,13 +109,13 @@
 
 val sync = "\\<^sync>";
 fun is_sync s = s = sync;
-fun not_sync s = s <> sync;
 
 val malformed = "[[";
 val end_malformed = "]]";
+fun malformed_msg s = "Malformed symbolic character: " ^ quote (Output.escape_malformed s);
 
-fun malformed_msg s =
-  "Malformed symbolic character: " ^ quote (Output.escape_malformed s);
+fun is_regular s =
+  not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
 
 
 (* ascii symbols *)
--- a/src/Pure/General/url.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/General/url.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -53,11 +53,11 @@
 local
 
 val scan_host =
-  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
+  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
-val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
+val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
+val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
 
 val scan_url =
   Scan.unless (Scan.this_string "file:" ||
--- a/src/Pure/Isar/antiquote.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/Isar/antiquote.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -39,7 +39,7 @@
 val scan_txt =
   T.scan_blank ||
   T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
-  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));
+  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.is_regular s));
 
 fun escape "\\" = "\\\\"
   | escape "\"" = "\\\""
@@ -50,7 +50,7 @@
 val scan_ant =
   T.scan_blank ||
   T.scan_string >> quote_escape ||
-  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.not_sync s andalso Symbol.not_eof s));
+  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
 
 val scan_antiq =
   T.keep_line ($$ "@" -- $$ "{") |--
--- a/src/Pure/Syntax/lexicon.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -216,7 +216,7 @@
 
 val scan_chr =
   $$ "\\" |-- $$ "'" ||
-  Scan.one (fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) ||
+  Scan.one (fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) ||
   $$ "'" --| Scan.ahead (~$$ "'");
 
 val scan_str =
@@ -238,7 +238,7 @@
   Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) ||
   Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) ||
   Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) ||
-  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.not_eof s));
+  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s));
 
 val scan_comment =
   $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
@@ -335,7 +335,7 @@
   let
     val scan =
       $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
-      Scan.many Symbol.not_eof >> (free o implode);
+      Scan.many Symbol.is_regular >> (free o implode);
   in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
 
 
@@ -413,7 +413,7 @@
 fun read_idents str =
   let
     val blanks = Scan.many Symbol.is_blank;
-    val junk = Scan.many Symbol.not_eof;
+    val junk = Scan.many Symbol.is_regular;
     val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
   in
     (case Scan.read Symbol.stopper idents (Symbol.explode str) of
--- a/src/Pure/Syntax/syn_ext.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -194,8 +194,8 @@
 val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
 
 val scan_delim_char =
-  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
-  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
+  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
+  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
 
 fun read_int ["0", "0"] = ~1
   | read_int cs = #1 (Library.read_int cs);
--- a/src/Pure/Tools/codegen_names.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -40,7 +40,7 @@
 fun purify_name upper_else_lower =
   let
     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
-    val is_junk = not o is_valid andf Symbol.not_eof;
+    val is_junk = not o is_valid andf Symbol.is_regular;
     val junk = Scan.many is_junk;
     val scan_valids = Symbol.scanner "Malformed input"
       ((junk |--
@@ -179,7 +179,7 @@
   explode
   (*should disappear as soon as hierarchical theory name spaces are available*)
   #> Symbol.scanner "Malformed name"
-      (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
+      (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
   #> implode
   #> NameSpace.explode
   #> map (purify_name true);
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -139,7 +139,7 @@
 
 fun parse_mixfix prep_arg s =
   let
-    val sym_any = Scan.one Symbol.not_eof;
+    val sym_any = Scan.one Symbol.is_regular;
     val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
       || ($$ "_" >> K (Arg BR))
--- a/src/Pure/Tools/xml.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/Tools/xml.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -122,28 +122,28 @@
 val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
 
 val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
-  (scan_special || Scan.one Symbol.not_eof)) >> implode;
+  (scan_special || Scan.one Symbol.is_regular)) >> implode;
 
 val parse_string = Scan.read Symbol.stopper parse_chars o explode;
 
 val parse_cdata = Scan.this_string "<![CDATA[" |--
-  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
+  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
     implode) --| Scan.this_string "]]>";
 
 val parse_att =
   Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
   (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
-    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
+    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
 
 val parse_comment = Scan.this_string "<!--" --
-  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
+  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
   Scan.this_string "-->";
 
 val scan_comment_whspc =
   (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
 
 val parse_pi = Scan.this_string "<?" |--
-  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.not_eof)) --|
+  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
   Scan.this_string "?>";
 
 fun parse_content xs =
@@ -169,7 +169,7 @@
 val parse_document =
   Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
     (Scan.repeat (Scan.unless ($$ ">")
-      (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
+      (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
   parse_elem;
 
 fun tree_of_string s =
--- a/src/Pure/codegen.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/codegen.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -1087,13 +1087,13 @@
       || $$ "\\<module>" >> K Module
       || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
       || $$ "{" |-- $$ "*" |-- Scan.repeat1
-           (   $$ "'" |-- Scan.one Symbol.not_eof
-            || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
+           (   $$ "'" |-- Scan.one Symbol.is_regular
+            || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.is_regular)) --|
          $$ "*" --| $$ "}" >> (Quote o rd o implode)
       || Scan.repeat1
-           (   $$ "'" |-- Scan.one Symbol.not_eof
+           (   $$ "'" |-- Scan.one Symbol.is_regular
             || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
-                 (Scan.one Symbol.not_eof)) >> (Pretty o str o implode)))
+                 (Scan.one Symbol.is_regular)) >> (Pretty o str o implode)))
        (Symbol.explode s) of
      (p, []) => p
    | _ => error ("Malformed annotation: " ^ quote s));
isabelle