more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
authorwenzelm
Wed Jul 10 16:25:26 2013 +0200 (2013-07-10)
changeset 526163ac2878764f9
parent 52610 78a64edf431f
child 52617 42e02ddd1568
more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
src/Pure/General/scan.scala
src/Pure/General/symbol.ML
src/Pure/General/symbol.scala
src/Pure/General/symbol_pos.ML
src/Pure/Syntax/lexicon.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/General/scan.scala	Fri Jul 12 13:12:21 2013 +0200
     1.2 +++ b/src/Pure/General/scan.scala	Wed Jul 10 16:25:26 2013 +0200
     1.3 @@ -348,7 +348,18 @@
     1.4      private def other_token(is_command: String => Boolean)
     1.5        : Parser[Token] =
     1.6      {
     1.7 -      val id = one(Symbol.is_letter) ~ many(Symbol.is_letdig) ^^ { case x ~ y => x + y }
     1.8 +      val letdigs1 = many1(Symbol.is_letdig)
     1.9 +      val sub_sup =
    1.10 +        one(s =>
    1.11 +          s == Symbol.sub_decoded || s == "\\<^sub>" ||
    1.12 +          s == Symbol.isub_decoded || s == "\\<^isub>" ||
    1.13 +          s == Symbol.sup_decoded || s == "\\<^sup>" ||
    1.14 +          s == Symbol.isup_decoded || s == "\\<^isup>")
    1.15 +      val id =
    1.16 +        one(Symbol.is_letter) ~
    1.17 +          (rep(letdigs1 | (sub_sup ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
    1.18 +        { case x ~ y => x + y }
    1.19 +
    1.20        val nat = many1(Symbol.is_digit)
    1.21        val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z }
    1.22        val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
     2.1 --- a/src/Pure/General/symbol.ML	Fri Jul 12 13:12:21 2013 +0200
     2.2 +++ b/src/Pure/General/symbol.ML	Wed Jul 10 16:25:26 2013 +0200
     2.3 @@ -46,7 +46,6 @@
     2.4    val decode: symbol -> sym
     2.5    datatype kind = Letter | Digit | Quasi | Blank | Other
     2.6    val kind: symbol -> kind
     2.7 -  val is_letter_symbol: symbol -> bool
     2.8    val is_letter: symbol -> bool
     2.9    val is_digit: symbol -> bool
    2.10    val is_quasi: symbol -> bool
    2.11 @@ -377,9 +376,7 @@
    2.12        "\\<Upsilon>",
    2.13        "\\<Phi>",
    2.14        "\\<Psi>",
    2.15 -      "\\<Omega>",
    2.16 -      "\\<^isub>",
    2.17 -      "\\<^isup>"
    2.18 +      "\\<Omega>"
    2.19      ];
    2.20  in
    2.21  
    2.22 @@ -520,6 +517,7 @@
    2.23  
    2.24  fun symbolic_end (_ :: "\\<^sub>" :: _) = true
    2.25    | symbolic_end (_ :: "\\<^isub>" :: _) = true
    2.26 +  | symbolic_end (_ :: "\\<^sup>" :: _) = true
    2.27    | symbolic_end (_ :: "\\<^isup>" :: _) = true
    2.28    | symbolic_end (s :: _) = is_symbolic s
    2.29    | symbolic_end [] = false;
     3.1 --- a/src/Pure/General/symbol.scala	Fri Jul 12 13:12:21 2013 +0200
     3.2 +++ b/src/Pure/General/symbol.scala	Wed Jul 10 16:25:26 2013 +0200
     3.3 @@ -347,9 +347,7 @@
     3.4        "\\<tau>", "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>",
     3.5        "\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>", "\\<Lambda>",
     3.6        "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
     3.7 -      "\\<Psi>", "\\<Omega>",
     3.8 -
     3.9 -      "\\<^isub>", "\\<^isup>")
    3.10 +      "\\<Psi>", "\\<Omega>")
    3.11  
    3.12      val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<^newline>")
    3.13  
     4.1 --- a/src/Pure/General/symbol_pos.ML	Fri Jul 12 13:12:21 2013 +0200
     4.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Jul 10 16:25:26 2013 +0200
     4.3 @@ -215,51 +215,19 @@
     4.4  
     4.5  local
     4.6  
     4.7 -val latin = Symbol.is_ascii_letter;
     4.8 -val digit = Symbol.is_ascii_digit;
     4.9 -fun underscore s = s = "_";
    4.10 -fun prime s = s = "'";
    4.11 -fun subscript s = s = "\\<^sub>" orelse s = "\\<^isub>";
    4.12 -fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
    4.13 -fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
    4.14 -
    4.15 -val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
    4.16 -val scan_digit = Scan.one (digit o symbol) >> single;
    4.17 -val scan_prime = Scan.one (prime o symbol) >> single;
    4.18 -val scan_extended =
    4.19 -  Scan.one ((latin orf digit orf prime orf underscore orf special_letter) o symbol) >> single;
    4.20 -
    4.21 -val scan_subscript =
    4.22 -  Scan.one (subscript o symbol) --
    4.23 -  Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
    4.24 -  >> (fn (x, y) => [x, y]);
    4.25 -
    4.26 -val scan_ident_part1 =
    4.27 -  Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_subscript) >> flat) ||
    4.28 -  Scan.one (special_letter o symbol) :::
    4.29 -    (Scan.repeat (scan_digit || scan_prime || scan_subscript) >> flat);
    4.30 -
    4.31 -val scan_ident_part2 =
    4.32 -  Scan.repeat1 (scan_plain || scan_subscript) >> flat ||
    4.33 -  scan_ident_part1;
    4.34 +val letter = Scan.one (symbol #> Symbol.is_letter);
    4.35 +val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
    4.36 +val sub_sup =
    4.37 +  Scan.one (symbol #>
    4.38 +    (fn s => s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^sup>" orelse s = "\\<^isup>"));
    4.39  
    4.40  in
    4.41  
    4.42 -val scan_ident0 =
    4.43 -  Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
    4.44 -
    4.45 -val scan_ident1 =
    4.46 -  Scan.one ((latin orf special_letter) o symbol) :::
    4.47 -    (Scan.repeat (scan_extended || Scan.one (subscript o symbol) ::: scan_extended) >> flat);
    4.48 -
    4.49 -val scan_ident2 =
    4.50 -  scan_ident_part1 @@@
    4.51 -    (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat);
    4.52 +val scan_ident =
    4.53 +  letter ::: (Scan.repeat (letdigs1 || sub_sup ::: letdigs1) >> flat);
    4.54  
    4.55  end;
    4.56  
    4.57 -val scan_ident = scan_ident0;
    4.58 -
    4.59  fun is_identifier s =
    4.60    Symbol.is_ascii_identifier s orelse
    4.61      (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of
     5.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Jul 12 13:12:21 2013 +0200
     5.2 +++ b/src/Pure/Syntax/lexicon.ML	Wed Jul 10 16:25:26 2013 +0200
     5.3 @@ -296,6 +296,7 @@
     5.4      fun chop_idx [] ds = idxname [] ds
     5.5        | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
     5.6        | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
     5.7 +      | chop_idx (cs as (_ :: "\\<^sup>" :: _)) ds = idxname cs ds
     5.8        | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
     5.9        | chop_idx (c :: cs) ds =
    5.10            if Symbol.is_digit c then chop_idx cs (c :: ds)
     6.1 --- a/src/Pure/term.ML	Fri Jul 12 13:12:21 2013 +0200
     6.2 +++ b/src/Pure/term.ML	Wed Jul 10 16:25:26 2013 +0200
     6.3 @@ -980,6 +980,7 @@
     6.4        (case rev (Symbol.explode x) of
     6.5          _ :: "\\<^sub>" :: _ => false
     6.6        | _ :: "\\<^isub>" :: _ => false
     6.7 +      | _ :: "\\<^sup>" :: _ => false
     6.8        | _ :: "\\<^isup>" :: _ => false
     6.9        | c :: _ => Symbol.is_digit c
    6.10        | _ => true);