eliminated slightly odd pervasive Symbol_Pos.symbol;
authorwenzelm
Sat Nov 13 19:47:23 2010 +0100 (2010-11-13)
changeset 4052514a2e686bdac
parent 40524 6131d7a78ad3
child 40526 ca3c6b1bfcdb
eliminated slightly odd pervasive Symbol_Pos.symbol;
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_lex.ML
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Sat Nov 13 19:27:41 2010 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Nov 13 19:47:23 2010 +0100
     1.3 @@ -182,7 +182,6 @@
     1.4  
     1.5  structure Basic_Symbol_Pos =   (*not open by default*)
     1.6  struct
     1.7 -  val symbol = Symbol_Pos.symbol;
     1.8    val $$$ = Symbol_Pos.$$$;
     1.9    val ~$$$ = Symbol_Pos.~$$$;
    1.10  end;
     2.1 --- a/src/Pure/Isar/token.ML	Sat Nov 13 19:27:41 2010 +0100
     2.2 +++ b/src/Pure/Isar/token.ML	Sat Nov 13 19:47:23 2010 +0100
     2.3 @@ -269,8 +269,8 @@
     2.4  val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
     2.5  
     2.6  val scan_symid =
     2.7 -  Scan.many1 (is_sym_char o symbol) ||
     2.8 -  Scan.one (Symbol.is_symbolic o symbol) >> single;
     2.9 +  Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
    2.10 +  Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
    2.11  
    2.12  fun is_symid str =
    2.13    (case try Symbol.explode str of
    2.14 @@ -301,8 +301,8 @@
    2.15  fun is_space s = Symbol.is_blank s andalso s <> "\n";
    2.16  
    2.17  val scan_space =
    2.18 -  Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
    2.19 -  Scan.many (is_space o symbol) @@@ $$$ "\n";
    2.20 +  Scan.many1 (is_space o Symbol_Pos.symbol) @@@ Scan.optional ($$$ "\n") [] ||
    2.21 +  Scan.many (is_space o Symbol_Pos.symbol) @@@ $$$ "\n";
    2.22  
    2.23  
    2.24  (* scan comment *)
    2.25 @@ -332,8 +332,8 @@
    2.26      scan_verbatim >> token_range Verbatim ||
    2.27      scan_comment >> token_range Comment ||
    2.28      scan_space >> token Space ||
    2.29 -    Scan.one (Symbol.is_malformed o symbol) >> (token Malformed o single) ||
    2.30 -    Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
    2.31 +    Scan.one (Symbol.is_malformed o Symbol_Pos.symbol) >> (token Malformed o single) ||
    2.32 +    Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
    2.33      (Scan.max token_leq
    2.34        (Scan.max token_leq
    2.35          (Scan.literal lex2 >> pair Command)
    2.36 @@ -348,7 +348,7 @@
    2.37          scan_symid >> pair SymIdent) >> uncurry token));
    2.38  
    2.39  fun recover msg =
    2.40 -  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
    2.41 +  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o Symbol_Pos.symbol)
    2.42    >> (single o token (Error msg));
    2.43  
    2.44  in
     3.1 --- a/src/Pure/ML/ml_lex.ML	Sat Nov 13 19:27:41 2010 +0100
     3.2 +++ b/src/Pure/ML/ml_lex.ML	Sat Nov 13 19:47:23 2010 +0100
     3.3 @@ -135,7 +135,7 @@
     3.4  
     3.5  (* blanks *)
     3.6  
     3.7 -val scan_blank = Scan.one (Symbol.is_ascii_blank o symbol);
     3.8 +val scan_blank = Scan.one (Symbol.is_ascii_blank o Symbol_Pos.symbol);
     3.9  val scan_blanks1 = Scan.repeat1 scan_blank;
    3.10  
    3.11  
    3.12 @@ -158,11 +158,15 @@
    3.13  local
    3.14  
    3.15  val scan_letdigs =
    3.16 -  Scan.many ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o symbol);
    3.17 +  Scan.many
    3.18 +    ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o
    3.19 +      Symbol_Pos.symbol);
    3.20  
    3.21 -val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o symbol) -- scan_letdigs >> op ::;
    3.22 +val scan_alphanumeric =
    3.23 +  Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;
    3.24  
    3.25 -val scan_symbolic = Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o symbol);
    3.26 +val scan_symbolic =
    3.27 +  Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
    3.28  
    3.29  in
    3.30  
    3.31 @@ -180,8 +184,8 @@
    3.32  
    3.33  local
    3.34  
    3.35 -val scan_dec = Scan.many1 (Symbol.is_ascii_digit o symbol);
    3.36 -val scan_hex = Scan.many1 (Symbol.is_ascii_hex o symbol);
    3.37 +val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol);
    3.38 +val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
    3.39  val scan_sign = Scan.optional ($$$ "~") [];
    3.40  val scan_decint = scan_sign @@@ scan_dec;
    3.41  
    3.42 @@ -207,11 +211,11 @@
    3.43  local
    3.44  
    3.45  val scan_escape =
    3.46 -  Scan.one (member (op =) (explode "\"\\abtnvfr") o symbol) >> single ||
    3.47 +  Scan.one (member (op =) (explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
    3.48    $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
    3.49 -  Scan.one (Symbol.is_ascii_digit o symbol) --
    3.50 -    Scan.one (Symbol.is_ascii_digit o symbol) --
    3.51 -    Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]);
    3.52 +  Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
    3.53 +    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
    3.54 +    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
    3.55  
    3.56  val scan_str =
    3.57    Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
    3.58 @@ -256,7 +260,7 @@
    3.59  val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
    3.60  
    3.61  fun recover msg =
    3.62 -  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
    3.63 +  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o Symbol_Pos.symbol)
    3.64    >> (fn cs => [token (Error msg) cs]);
    3.65  
    3.66  in
     4.1 --- a/src/Pure/Syntax/lexicon.ML	Sat Nov 13 19:27:41 2010 +0100
     4.2 +++ b/src/Pure/Syntax/lexicon.ML	Sat Nov 13 19:47:23 2010 +0100
     4.3 @@ -103,15 +103,18 @@
     4.4  
     4.5  fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
     4.6  
     4.7 -val scan_id = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
     4.8 +val scan_id =
     4.9 +  Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::
    4.10 +  Scan.many (Symbol.is_letdig o Symbol_Pos.symbol);
    4.11 +
    4.12  val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
    4.13  val scan_tid = $$$ "'" @@@ scan_id;
    4.14  
    4.15 -val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
    4.16 +val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
    4.17  val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
    4.18  val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
    4.19  val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
    4.20 -val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o symbol);
    4.21 +val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
    4.22  val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
    4.23  
    4.24  val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
    4.25 @@ -221,7 +224,9 @@
    4.26  
    4.27  val scan_chr =
    4.28    $$$ "\\" |-- $$$ "'" ||
    4.29 -  Scan.one ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o symbol) >> single ||
    4.30 +  Scan.one
    4.31 +    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
    4.32 +      Symbol_Pos.symbol) >> single ||
    4.33    $$$ "'" --| Scan.ahead (~$$$ "'");
    4.34  
    4.35  val scan_str =
    4.36 @@ -237,7 +242,7 @@
    4.37  
    4.38  fun explode_xstr str =
    4.39    (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
    4.40 -    SOME cs => map symbol cs
    4.41 +    SOME cs => map Symbol_Pos.symbol cs
    4.42    | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
    4.43  
    4.44  
    4.45 @@ -271,7 +276,7 @@
    4.46        Symbol_Pos.scan_comment !!! >> token Comment ||
    4.47        Scan.max token_leq scan_lit scan_val ||
    4.48        scan_str >> token StrSy ||
    4.49 -      Scan.many1 (Symbol.is_blank o symbol) >> token Space;
    4.50 +      Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
    4.51    in
    4.52      (case Scan.error
    4.53          (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
    4.54 @@ -301,8 +306,8 @@
    4.55            if Symbol.is_digit c then chop_idx cs (c :: ds)
    4.56            else idxname (c :: cs) ds;
    4.57  
    4.58 -    val scan = (scan_id >> map symbol) --
    4.59 -      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map symbol)) ~1;
    4.60 +    val scan = (scan_id >> map Symbol_Pos.symbol) --
    4.61 +      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
    4.62    in
    4.63      scan >>
    4.64        (fn (cs, ~1) => chop_idx (rev cs) []
    4.65 @@ -334,7 +339,7 @@
    4.66    let
    4.67      val scan =
    4.68        $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
    4.69 -      Scan.many (Symbol.is_regular o symbol) >> (free o implode o map symbol);
    4.70 +      Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (free o implode o map Symbol_Pos.symbol);
    4.71    in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
    4.72  
    4.73  
    4.74 @@ -378,7 +383,7 @@
    4.75  local
    4.76  
    4.77  fun nat cs =
    4.78 -  Option.map (#1 o Library.read_int o map symbol)
    4.79 +  Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
    4.80      (Scan.read Symbol_Pos.stopper scan_nat cs);
    4.81  
    4.82  in