more systematic mark/unmark operations;
authorwenzelm
Wed Mar 03 00:00:44 2010 +0100 (2010-03-03)
changeset 35428bd7d6f65976e
parent 35427 ad039d29e01c
child 35429 afa8cf9e63d8
more systematic mark/unmark operations;
tuned;
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Mar 02 23:59:54 2010 +0100
     1.2 +++ b/src/Pure/Syntax/lexicon.ML	Wed Mar 03 00:00:44 2010 +0100
     1.3 @@ -30,12 +30,17 @@
     1.4    val read_int: string -> int option
     1.5    val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
     1.6    val read_float: string -> {mant: int, exp: int}
     1.7 -  val fixedN: string
     1.8 -  val mark_fixed: string -> string
     1.9 -  val unmark_fixed: string -> string
    1.10 -  val constN: string
    1.11 -  val mark_const: string -> string
    1.12 -  val unmark_const: string -> string
    1.13 +  val mark_class: string -> string val unmark_class: string -> string
    1.14 +  val mark_type: string -> string val unmark_type: string -> string
    1.15 +  val mark_const: string -> string val unmark_const: string -> string
    1.16 +  val mark_fixed: string -> string val unmark_fixed: string -> string
    1.17 +  val unmark:
    1.18 +   {case_class: string -> 'a,
    1.19 +    case_type: string -> 'a,
    1.20 +    case_const: string -> 'a,
    1.21 +    case_fixed: string -> 'a,
    1.22 +    case_default: string -> 'a} -> string -> 'a
    1.23 +  val is_marked: string -> bool
    1.24  end;
    1.25  
    1.26  signature LEXICON =
    1.27 @@ -333,15 +338,32 @@
    1.28    in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
    1.29  
    1.30  
    1.31 -(* specific identifiers *)
    1.32 +(* logical entities *)
    1.33 +
    1.34 +fun marker s = (prefix s, unprefix s);
    1.35 +
    1.36 +val (mark_class, unmark_class) = marker "\\<^class>";
    1.37 +val (mark_type, unmark_type) = marker "\\<^type>";
    1.38 +val (mark_const, unmark_const) = marker "\\<^const>";
    1.39 +val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
    1.40  
    1.41 -val fixedN = "\\<^fixed>";
    1.42 -val mark_fixed = prefix fixedN;
    1.43 -val unmark_fixed = unprefix fixedN;
    1.44 +fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
    1.45 +  (case try unmark_class s of
    1.46 +    SOME c => case_class c
    1.47 +  | NONE =>
    1.48 +      (case try unmark_type s of
    1.49 +        SOME c => case_type c
    1.50 +      | NONE =>
    1.51 +          (case try unmark_const s of
    1.52 +            SOME c => case_const c
    1.53 +          | NONE =>
    1.54 +              (case try unmark_fixed s of
    1.55 +                SOME c => case_fixed c
    1.56 +              | NONE => case_default s))));
    1.57  
    1.58 -val constN = "\\<^const>";
    1.59 -val mark_const = prefix constN;
    1.60 -val unmark_const = unprefix constN;
    1.61 +val is_marked =
    1.62 +  unmark {case_class = K true, case_type = K true, case_const = K true,
    1.63 +    case_fixed = K true, case_default = K false};
    1.64  
    1.65  
    1.66  (* read numbers *)
    1.67 @@ -371,7 +393,7 @@
    1.68  val ten = ord "0" + 10;
    1.69  val a = ord "a";
    1.70  val A = ord "A";
    1.71 -val _ = a > A orelse sys_error "Bad ASCII";
    1.72 +val _ = a > A orelse raise Fail "Bad ASCII";
    1.73  
    1.74  fun remap_hex c =
    1.75    let val x = ord c in