# HG changeset patch # User wenzelm # Date 1373466326 -7200 # Node ID 3ac2878764f9adc681826f90e6ceeed202778dc8 # Parent 78a64edf431fa2cd66823ba4ed7b044f0d3b2dc0 more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed; diff -r 78a64edf431f -r 3ac2878764f9 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Fri Jul 12 13:12:21 2013 +0200 +++ b/src/Pure/General/scan.scala Wed Jul 10 16:25:26 2013 +0200 @@ -348,7 +348,18 @@ private def other_token(is_command: String => Boolean) : Parser[Token] = { - val id = one(Symbol.is_letter) ~ many(Symbol.is_letdig) ^^ { case x ~ y => x + y } + val letdigs1 = many1(Symbol.is_letdig) + val sub_sup = + one(s => + s == Symbol.sub_decoded || s == "\\<^sub>" || + s == Symbol.isub_decoded || s == "\\<^isub>" || + s == Symbol.sup_decoded || s == "\\<^sup>" || + s == Symbol.isup_decoded || s == "\\<^isup>") + val id = + one(Symbol.is_letter) ~ + (rep(letdigs1 | (sub_sup ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^ + { case x ~ y => x + y } + val nat = many1(Symbol.is_digit) val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z } val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x } diff -r 78a64edf431f -r 3ac2878764f9 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Fri Jul 12 13:12:21 2013 +0200 +++ b/src/Pure/General/symbol.ML Wed Jul 10 16:25:26 2013 +0200 @@ -46,7 +46,6 @@ 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 @@ -377,9 +376,7 @@ "\\", "\\", "\\", - "\\", - "\\<^isub>", - "\\<^isup>" + "\\" ]; in @@ -520,6 +517,7 @@ fun symbolic_end (_ :: "\\<^sub>" :: _) = true | symbolic_end (_ :: "\\<^isub>" :: _) = true + | symbolic_end (_ :: "\\<^sup>" :: _) = true | symbolic_end (_ :: "\\<^isup>" :: _) = true | symbolic_end (s :: _) = is_symbolic s | symbolic_end [] = false; diff -r 78a64edf431f -r 3ac2878764f9 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Jul 12 13:12:21 2013 +0200 +++ b/src/Pure/General/symbol.scala Wed Jul 10 16:25:26 2013 +0200 @@ -347,9 +347,7 @@ "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", - "\\", "\\", - - "\\<^isub>", "\\<^isup>") + "\\", "\\") val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<^newline>") diff -r 78a64edf431f -r 3ac2878764f9 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Fri Jul 12 13:12:21 2013 +0200 +++ b/src/Pure/General/symbol_pos.ML Wed Jul 10 16:25:26 2013 +0200 @@ -215,51 +215,19 @@ local -val latin = Symbol.is_ascii_letter; -val digit = Symbol.is_ascii_digit; -fun underscore s = s = "_"; -fun prime s = s = "'"; -fun subscript s = s = "\\<^sub>" orelse s = "\\<^isub>"; -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_extended = - Scan.one ((latin orf digit orf prime orf underscore orf special_letter) o symbol) >> single; - -val scan_subscript = - Scan.one (subscript o symbol) -- - Scan.one ((latin orf digit orf prime orf special_letter) o symbol) - >> (fn (x, y) => [x, y]); - -val scan_ident_part1 = - Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_subscript) >> flat) || - Scan.one (special_letter o symbol) ::: - (Scan.repeat (scan_digit || scan_prime || scan_subscript) >> flat); - -val scan_ident_part2 = - Scan.repeat1 (scan_plain || scan_subscript) >> flat || - scan_ident_part1; +val letter = Scan.one (symbol #> Symbol.is_letter); +val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig); +val sub_sup = + Scan.one (symbol #> + (fn s => s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^sup>" orelse s = "\\<^isup>")); in -val scan_ident0 = - Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol); - -val scan_ident1 = - Scan.one ((latin orf special_letter) o symbol) ::: - (Scan.repeat (scan_extended || Scan.one (subscript o symbol) ::: scan_extended) >> flat); - -val scan_ident2 = - scan_ident_part1 @@@ - (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat); +val scan_ident = + letter ::: (Scan.repeat (letdigs1 || sub_sup ::: letdigs1) >> flat); end; -val scan_ident = scan_ident0; - fun is_identifier s = Symbol.is_ascii_identifier s orelse (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of diff -r 78a64edf431f -r 3ac2878764f9 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Fri Jul 12 13:12:21 2013 +0200 +++ b/src/Pure/Syntax/lexicon.ML Wed Jul 10 16:25:26 2013 +0200 @@ -296,6 +296,7 @@ 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 (_ :: "\\<^sup>" :: _)) ds = idxname cs ds | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds | chop_idx (c :: cs) ds = if Symbol.is_digit c then chop_idx cs (c :: ds) diff -r 78a64edf431f -r 3ac2878764f9 src/Pure/term.ML --- a/src/Pure/term.ML Fri Jul 12 13:12:21 2013 +0200 +++ b/src/Pure/term.ML Wed Jul 10 16:25:26 2013 +0200 @@ -980,6 +980,7 @@ (case rev (Symbol.explode x) of _ :: "\\<^sub>" :: _ => false | _ :: "\\<^isub>" :: _ => false + | _ :: "\\<^sup>" :: _ => false | _ :: "\\<^isup>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true);