# HG changeset patch
# User wenzelm
# Date 1354040556 -3600
# Node ID 56b9c792a98b03f48543389dd1e22b828ceee0c8
# Parent  8b0fdeeefef7232b8818cca90bf56e08c70344cf
support for sub-structured identifier syntax (inactive);

diff -r 8b0fdeeefef7 -r 56b9c792a98b src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Nov 27 13:22:29 2012 +0100
+++ b/src/Pure/General/symbol.ML	Tue Nov 27 19:22:36 2012 +0100
@@ -46,6 +46,7 @@
   val decode: symbol -> sym
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
+  val is_letter_symbol: symbol -> bool
   val is_letter: symbol -> bool
   val is_digit: symbol -> bool
   val is_quasi: symbol -> bool
@@ -236,8 +237,6 @@
 
 (* standard symbol kinds *)
 
-datatype kind = Letter | Digit | Quasi | Blank | Other;
-
 local
   val letter_symbols =
     Symtab.make_set [
@@ -383,16 +382,22 @@
       "\\<^isup>"
     ];
 in
-  fun kind s =
-    if is_ascii_letter s then Letter
-    else if is_ascii_digit s then Digit
-    else if is_ascii_quasi s then Quasi
-    else if is_ascii_blank s then Blank
-    else if is_char s then Other
-    else if Symtab.defined letter_symbols s then Letter
-    else Other;
+
+val is_letter_symbol = Symtab.defined letter_symbols;
+
 end;
 
+datatype kind = Letter | Digit | Quasi | Blank | Other;
+
+fun kind s =
+  if is_ascii_letter s then Letter
+  else if is_ascii_digit s then Digit
+  else if is_ascii_quasi s then Quasi
+  else if is_ascii_blank s then Blank
+  else if is_char s then Other
+  else if is_letter_symbol s then Letter
+  else Other;
+
 fun is_letter s = kind s = Letter;
 fun is_digit s = kind s = Digit;
 fun is_quasi s = kind s = Quasi;
@@ -513,7 +518,8 @@
 
 (* bump string -- treat as base 26 or base 1 numbers *)
 
-fun symbolic_end (_ :: "\\<^isub>" :: _) = true
+fun symbolic_end (_ :: "\\<^sub>" :: _) = true
+  | symbolic_end (_ :: "\\<^isub>" :: _) = true
   | symbolic_end (_ :: "\\<^isup>" :: _) = true
   | symbolic_end (s :: _) = is_symbolic s
   | symbolic_end [] = false;
diff -r 8b0fdeeefef7 -r 56b9c792a98b src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Tue Nov 27 13:22:29 2012 +0100
+++ b/src/Pure/General/symbol_pos.ML	Tue Nov 27 19:22:36 2012 +0100
@@ -37,8 +37,8 @@
   val range: T list -> Position.range
   val implode_range: Position.T -> Position.T -> T list -> text * Position.range
   val explode: text * Position.T -> T list
+  val scan_new_ident: T list -> T list * T list
   val scan_ident: T list -> T list * T list
-  val is_ident: T list -> bool
   val is_identifier: string -> bool
 end;
 
@@ -214,6 +214,40 @@
 
 (* identifiers *)
 
+local
+
+val latin = Symbol.is_ascii_letter;
+val digit = Symbol.is_ascii_digit;
+fun underscore s = s = "_";
+fun prime s = s = "'";
+fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
+fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
+
+val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
+val scan_digit = Scan.one (digit o symbol) >> single;
+val scan_prime = Scan.one (prime o symbol) >> single;
+
+val scan_script =
+  Scan.one (script o symbol) -- Scan.one ((latin orf digit orf special_letter) o symbol)
+  >> (fn (x, y) => [x, y]);
+
+val scan_ident_part1 =
+  Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_script) >> flat) ||
+  Scan.one (special_letter o symbol) :::
+    (Scan.repeat (scan_digit || scan_prime || scan_script) >> flat);
+
+val scan_ident_part2 =
+  Scan.repeat1 (scan_plain || scan_script) >> flat ||
+  scan_ident_part1;
+
+in
+
+val scan_new_ident =
+  scan_ident_part1 @@@
+    (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat);
+
+end;
+
 val scan_ident =
   Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
 
diff -r 8b0fdeeefef7 -r 56b9c792a98b src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Nov 27 13:22:29 2012 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Nov 27 19:22:36 2012 +0100
@@ -293,6 +293,7 @@
 
     fun idxname cs ds = (implode (rev cs), nat 0 ds);
     fun chop_idx [] ds = idxname [] ds
+      | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
       | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
       | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
       | chop_idx (c :: cs) ds =
diff -r 8b0fdeeefef7 -r 56b9c792a98b src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Nov 27 13:22:29 2012 +0100
+++ b/src/Pure/term.ML	Tue Nov 27 19:22:36 2012 +0100
@@ -981,7 +981,8 @@
     val idx = string_of_int i;
     val dot =
       (case rev (Symbol.explode x) of
-        _ :: "\\<^isub>" :: _ => false
+        _ :: "\\<^sub>" :: _ => false
+      | _ :: "\\<^isub>" :: _ => false
       | _ :: "\\<^isup>" :: _ => false
       | c :: _ => Symbol.is_digit c
       | _ => true);