src/Pure/Isar/token.scala

 
 import scala.collection.mutable
 import scala.util.parsing.input
 
 
-object Token
-{
+object Token {
   /* tokens */
 
-  object Kind extends Enumeration
-  {
+  object Kind extends Enumeration {
     /*immediate source*/
     val COMMAND = Value("command")
     val KEYWORD = Value("keyword")
     val IDENT = Value("identifier")
     val LONG_IDENT = Value("long identifier")

 
   /* parsers */
 
   object Parsers extends Parsers
 
-  trait Parsers extends Scan.Parsers with Comment.Parsers
-  {
-    private def delimited_token: Parser[Token] =
-    {
+  trait Parsers extends Scan.Parsers with Comment.Parsers {
+    private def delimited_token: Parser[Token] = {
       val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
       val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
       val cmt = comment ^^ (x => Token(Token.Kind.INFORMAL_COMMENT, x))
       val formal_cmt = comment_cartouche ^^ (x => Token(Token.Kind.FORMAL_COMMENT, x))
       val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
       val ctrl = control_cartouche ^^ (x => Token(Token.Kind.CONTROL, x))
 
       string | (alt_string | (cmt | (formal_cmt | (cart | ctrl))))
     }
 
-    private def other_token(keywords: Keyword.Keywords): Parser[Token] =
-    {
+    private def other_token(keywords: Keyword.Keywords): Parser[Token] = {
       val letdigs1 = many1(Symbol.is_letdig)
       val sub = one(s => s == Symbol.sub_decoded || s == Symbol.sub)
       val id =
         one(Symbol.is_letter) ~
           (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^

     }
 
     def token(keywords: Keyword.Keywords): Parser[Token] =
       delimited_token | other_token(keywords)
 
-    def token_line(keywords: Keyword.Keywords, ctxt: Scan.Line_Context)
-      : Parser[(Token, Scan.Line_Context)] =
-    {
+    def token_line(
+      keywords: Keyword.Keywords,
+      ctxt: Scan.Line_Context
+    ) : Parser[(Token, Scan.Line_Context)] = {
       val string =
         quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
       val alt_string =
         quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
       val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }

     Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), Scan.char_reader(inp)) match {
       case Parsers.Success(tokens, _) => tokens
       case _ => error("Unexpected failure of tokenizing input:\n" + inp.toString)
     }
 
-  def explode_line(keywords: Keyword.Keywords, inp: CharSequence, context: Scan.Line_Context)
-    : (List[Token], Scan.Line_Context) =
-  {
+  def explode_line(
+    keywords: Keyword.Keywords,
+    inp: CharSequence,
+    context: Scan.Line_Context
+  ) : (List[Token], Scan.Line_Context) = {
     var in: input.Reader[Char] = Scan.char_reader(inp)
     val toks = new mutable.ListBuffer[Token]
     var ctxt = context
     while (!in.atEnd) {
       Parsers.parse(Parsers.token_line(keywords, ctxt), in) match {

     }
 
 
   /* token reader */
 
-  object Pos
-  {
+  object Pos {
     val none: Pos = new Pos(0, 0, "", "")
     val start: Pos = new Pos(1, 1, "", "")
     def file(file: String): Pos = new Pos(1, 1, file, "")
     def id(id: String): Pos = new Pos(0, 1, "", id)
     val command: Pos = id(Markup.COMMAND)

   final class Pos private[Token](
       val line: Int,
       val offset: Symbol.Offset,
       val file: String,
       val id: String)
-    extends input.Position
-  {
+  extends input.Position {
     def column = 0
     def lineContents = ""
 
     def advance(token: Token): Pos = advance(token.source)
-    def advance(source: String): Pos =
-    {
+    def advance(source: String): Pos = {
       var line1 = line
       var offset1 = offset
       for (s <- Symbol.iterator(source)) {
         if (line1 > 0 && Symbol.is_newline(s)) line1 += 1
         if (offset1 > 0) offset1 += 1

     override def toString: String = Position.here(position(), delimited = false)
   }
 
   abstract class Reader extends input.Reader[Token]
 
-  private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader
-  {
+  private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader {
     def first: Token = tokens.head
     def rest: Token_Reader = new Token_Reader(tokens.tail, pos.advance(first))
     def atEnd: Boolean = tokens.isEmpty
   }
 
   def reader(tokens: List[Token], start: Token.Pos): Reader =
     new Token_Reader(tokens, start)
 }
 
 
-sealed case class Token(kind: Token.Kind.Value, source: String)
-{
+sealed case class Token(kind: Token.Kind.Value, source: String) {
   def is_command: Boolean = kind == Token.Kind.COMMAND
   def is_command(name: String): Boolean = kind == Token.Kind.COMMAND && source == name
   def is_keyword: Boolean = kind == Token.Kind.KEYWORD
   def is_keyword(name: String): Boolean = kind == Token.Kind.KEYWORD && source == name
   def is_keyword(name: Char): Boolean =

     else if (kind == Token.Kind.CARTOUCHE) Scan.Parsers.cartouche_content(source)
     else if (kind == Token.Kind.INFORMAL_COMMENT) Scan.Parsers.comment_content(source)
     else if (kind == Token.Kind.FORMAL_COMMENT) Comment.content(source)
     else source
 
-  def is_system_name: Boolean =
-  {
+  def is_system_name: Boolean = {
     val s = content
     is_name && Path.is_wellformed(s) &&
       !s.exists(Symbol.is_ascii_blank) &&
       !Path.is_reserved(s)
   }