support for sub-structured identifier syntax (inactive);
authorwenzelm
Tue Nov 27 19:22:36 2012 +0100 (2012-11-27)
changeset 5024256b9c792a98b
parent 50241 8b0fdeeefef7
child 50246 4df875d326ee
support for sub-structured identifier syntax (inactive);
src/Pure/General/symbol.ML
src/Pure/General/symbol_pos.ML
src/Pure/Syntax/lexicon.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/General/symbol.ML	Tue Nov 27 13:22:29 2012 +0100
     1.2 +++ b/src/Pure/General/symbol.ML	Tue Nov 27 19:22:36 2012 +0100
     1.3 @@ -46,6 +46,7 @@
     1.4    val decode: symbol -> sym
     1.5    datatype kind = Letter | Digit | Quasi | Blank | Other
     1.6    val kind: symbol -> kind
     1.7 +  val is_letter_symbol: symbol -> bool
     1.8    val is_letter: symbol -> bool
     1.9    val is_digit: symbol -> bool
    1.10    val is_quasi: symbol -> bool
    1.11 @@ -236,8 +237,6 @@
    1.12  
    1.13  (* standard symbol kinds *)
    1.14  
    1.15 -datatype kind = Letter | Digit | Quasi | Blank | Other;
    1.16 -
    1.17  local
    1.18    val letter_symbols =
    1.19      Symtab.make_set [
    1.20 @@ -383,16 +382,22 @@
    1.21        "\\<^isup>"
    1.22      ];
    1.23  in
    1.24 -  fun kind s =
    1.25 -    if is_ascii_letter s then Letter
    1.26 -    else if is_ascii_digit s then Digit
    1.27 -    else if is_ascii_quasi s then Quasi
    1.28 -    else if is_ascii_blank s then Blank
    1.29 -    else if is_char s then Other
    1.30 -    else if Symtab.defined letter_symbols s then Letter
    1.31 -    else Other;
    1.32 +
    1.33 +val is_letter_symbol = Symtab.defined letter_symbols;
    1.34 +
    1.35  end;
    1.36  
    1.37 +datatype kind = Letter | Digit | Quasi | Blank | Other;
    1.38 +
    1.39 +fun kind s =
    1.40 +  if is_ascii_letter s then Letter
    1.41 +  else if is_ascii_digit s then Digit
    1.42 +  else if is_ascii_quasi s then Quasi
    1.43 +  else if is_ascii_blank s then Blank
    1.44 +  else if is_char s then Other
    1.45 +  else if is_letter_symbol s then Letter
    1.46 +  else Other;
    1.47 +
    1.48  fun is_letter s = kind s = Letter;
    1.49  fun is_digit s = kind s = Digit;
    1.50  fun is_quasi s = kind s = Quasi;
    1.51 @@ -513,7 +518,8 @@
    1.52  
    1.53  (* bump string -- treat as base 26 or base 1 numbers *)
    1.54  
    1.55 -fun symbolic_end (_ :: "\\<^isub>" :: _) = true
    1.56 +fun symbolic_end (_ :: "\\<^sub>" :: _) = true
    1.57 +  | symbolic_end (_ :: "\\<^isub>" :: _) = true
    1.58    | symbolic_end (_ :: "\\<^isup>" :: _) = true
    1.59    | symbolic_end (s :: _) = is_symbolic s
    1.60    | symbolic_end [] = false;
     2.1 --- a/src/Pure/General/symbol_pos.ML	Tue Nov 27 13:22:29 2012 +0100
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Nov 27 19:22:36 2012 +0100
     2.3 @@ -37,8 +37,8 @@
     2.4    val range: T list -> Position.range
     2.5    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
     2.6    val explode: text * Position.T -> T list
     2.7 +  val scan_new_ident: T list -> T list * T list
     2.8    val scan_ident: T list -> T list * T list
     2.9 -  val is_ident: T list -> bool
    2.10    val is_identifier: string -> bool
    2.11  end;
    2.12  
    2.13 @@ -214,6 +214,40 @@
    2.14  
    2.15  (* identifiers *)
    2.16  
    2.17 +local
    2.18 +
    2.19 +val latin = Symbol.is_ascii_letter;
    2.20 +val digit = Symbol.is_ascii_digit;
    2.21 +fun underscore s = s = "_";
    2.22 +fun prime s = s = "'";
    2.23 +fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
    2.24 +fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
    2.25 +
    2.26 +val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
    2.27 +val scan_digit = Scan.one (digit o symbol) >> single;
    2.28 +val scan_prime = Scan.one (prime o symbol) >> single;
    2.29 +
    2.30 +val scan_script =
    2.31 +  Scan.one (script o symbol) -- Scan.one ((latin orf digit orf special_letter) o symbol)
    2.32 +  >> (fn (x, y) => [x, y]);
    2.33 +
    2.34 +val scan_ident_part1 =
    2.35 +  Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_script) >> flat) ||
    2.36 +  Scan.one (special_letter o symbol) :::
    2.37 +    (Scan.repeat (scan_digit || scan_prime || scan_script) >> flat);
    2.38 +
    2.39 +val scan_ident_part2 =
    2.40 +  Scan.repeat1 (scan_plain || scan_script) >> flat ||
    2.41 +  scan_ident_part1;
    2.42 +
    2.43 +in
    2.44 +
    2.45 +val scan_new_ident =
    2.46 +  scan_ident_part1 @@@
    2.47 +    (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat);
    2.48 +
    2.49 +end;
    2.50 +
    2.51  val scan_ident =
    2.52    Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
    2.53  
     3.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Nov 27 13:22:29 2012 +0100
     3.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Nov 27 19:22:36 2012 +0100
     3.3 @@ -293,6 +293,7 @@
     3.4  
     3.5      fun idxname cs ds = (implode (rev cs), nat 0 ds);
     3.6      fun chop_idx [] ds = idxname [] ds
     3.7 +      | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
     3.8        | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
     3.9        | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
    3.10        | chop_idx (c :: cs) ds =
     4.1 --- a/src/Pure/term.ML	Tue Nov 27 13:22:29 2012 +0100
     4.2 +++ b/src/Pure/term.ML	Tue Nov 27 19:22:36 2012 +0100
     4.3 @@ -981,7 +981,8 @@
     4.4      val idx = string_of_int i;
     4.5      val dot =
     4.6        (case rev (Symbol.explode x) of
     4.7 -        _ :: "\\<^isub>" :: _ => false
     4.8 +        _ :: "\\<^sub>" :: _ => false
     4.9 +      | _ :: "\\<^isub>" :: _ => false
    4.10        | _ :: "\\<^isup>" :: _ => false
    4.11        | c :: _ => Symbol.is_digit c
    4.12        | _ => true);