src/Pure/General/scan.scala

 /*  Title:      Pure/General/scan.scala
     Author:     Makarius
 
-Efficient scanning of keywords.
+Efficient scanning of keywords and tokens.
 */
 
 package isabelle
 
 

     /* quoted strings */
 
     private def quoted(quote: String): Parser[String] =
     {
       quote ~
-        rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_wellformed(sym)) |
-          "\\" + quote | "\\\\" |
+        rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
           (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ~
       quote ^^ { case x ~ ys ~ z => x + ys.mkString + z }
     }.named("quoted")
 
     def quoted_content(quote: String, source: String): String =
     {
       require(parseAll(quoted(quote), source).successful)
       val body = source.substring(1, source.length - 1)
       if (body.exists(_ == '\\')) {
         val content =
-          rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_wellformed(sym)) |
+          rep(many1(sym => sym != quote && sym != "\\") |
               "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString }))
         parseAll(content ^^ (_.mkString), body).get
       }
       else body
     }

 
     /* verbatim text */
 
     private def verbatim: Parser[String] =
     {
-      "{*" ~ rep(many1(sym => sym != "*" && Symbol.is_wellformed(sym)) | """\*(?!\})""".r) ~ "*}" ^^
+      "{*" ~ rep(many1(sym => sym != "*") | """\*(?!\})""".r) ~ "*}" ^^
         { case x ~ ys ~ z => x + ys.mkString + z }
     }.named("verbatim")
 
     def verbatim_content(source: String): String =
     {

     /* nested comments */
 
     def comment: Parser[String] = new Parser[String]
     {
       val comment_text =
-        rep(many1(sym => sym != "*" && sym != "(" && Symbol.is_wellformed(sym)) |
-          """\*(?!\))|\((?!\*)""".r)
+        rep(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
       val comment_open = "(*" ~ comment_text ^^^ ()
       val comment_close = comment_text ~ "*)" ^^^ ()
 
       def apply(in: Input) =
       {

       val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x))
       val float =
         ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
 
       val sym_ident =
-        (many1(symbols.is_symbolic_char) |
-          one(sym => symbols.is_symbolic(sym) & Symbol.is_wellformed(sym))) ^^
+        (many1(symbols.is_symbolic_char) | one(sym => symbols.is_symbolic(sym))) ^^
         (x => Token(Token.Kind.SYM_IDENT, x))
 
       val space = many1(symbols.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
 
       val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))