1.1 --- a/src/Pure/Isar/outer_lex.scala	Mon May 17 18:59:59 2010 -0700
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,94 +0,0 @@
     1.4 -/*  Title:      Pure/Isar/outer_lex.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Outer lexical syntax for Isabelle/Isar.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -
    1.13 -object Outer_Lex
    1.14 -{
    1.15 -  /* tokens */
    1.16 -
    1.17 -  object Token_Kind extends Enumeration
    1.18 -  {
    1.19 -    val COMMAND = Value("command")
    1.20 -    val KEYWORD = Value("keyword")
    1.21 -    val IDENT = Value("identifier")
    1.22 -    val LONG_IDENT = Value("long identifier")
    1.23 -    val SYM_IDENT = Value("symbolic identifier")
    1.24 -    val VAR = Value("schematic variable")
    1.25 -    val TYPE_IDENT = Value("type variable")
    1.26 -    val TYPE_VAR = Value("schematic type variable")
    1.27 -    val NAT = Value("number")
    1.28 -    val STRING = Value("string")
    1.29 -    val ALT_STRING = Value("back-quoted string")
    1.30 -    val VERBATIM = Value("verbatim text")
    1.31 -    val SPACE = Value("white space")
    1.32 -    val COMMENT = Value("comment text")
    1.33 -    val BAD_INPUT = Value("bad input")
    1.34 -    val UNPARSED = Value("unparsed input")
    1.35 -  }
    1.36 -
    1.37 -  sealed case class Token(val kind: Token_Kind.Value, val source: String)
    1.38 -  {
    1.39 -    def is_command: Boolean = kind == Token_Kind.COMMAND
    1.40 -    def is_delimited: Boolean =
    1.41 -      kind == Token_Kind.STRING ||
    1.42 -      kind == Token_Kind.ALT_STRING ||
    1.43 -      kind == Token_Kind.VERBATIM ||
    1.44 -      kind == Token_Kind.COMMENT
    1.45 -    def is_name: Boolean =
    1.46 -      kind == Token_Kind.IDENT ||
    1.47 -      kind == Token_Kind.SYM_IDENT ||
    1.48 -      kind == Token_Kind.STRING ||
    1.49 -      kind == Token_Kind.NAT
    1.50 -    def is_xname: Boolean = is_name || kind == Token_Kind.LONG_IDENT
    1.51 -    def is_text: Boolean = is_xname || kind == Token_Kind.VERBATIM
    1.52 -    def is_space: Boolean = kind == Token_Kind.SPACE
    1.53 -    def is_comment: Boolean = kind == Token_Kind.COMMENT
    1.54 -    def is_ignored: Boolean = is_space || is_comment
    1.55 -    def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
    1.56 -
    1.57 -    def content: String =
    1.58 -      if (kind == Token_Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
    1.59 -      else if (kind == Token_Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
    1.60 -      else if (kind == Token_Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
    1.61 -      else if (kind == Token_Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
    1.62 -      else source
    1.63 -
    1.64 -    def text: (String, String) =
    1.65 -      if (kind == Token_Kind.COMMAND && source == ";") ("terminator", "")
    1.66 -      else (kind.toString, source)
    1.67 -  }
    1.68 -
    1.69 -
    1.70 -  /* token reader */
    1.71 -
    1.72 -  class Line_Position(val line: Int) extends scala.util.parsing.input.Position
    1.73 -  {
    1.74 -    def column = 0
    1.75 -    def lineContents = ""
    1.76 -    override def toString = line.toString
    1.77 -
    1.78 -    def advance(token: Token): Line_Position =
    1.79 -    {
    1.80 -      var n = 0
    1.81 -      for (c <- token.content if c == '\n') n += 1
    1.82 -      if (n == 0) this else new Line_Position(line + n)
    1.83 -    }
    1.84 -  }
    1.85 -
    1.86 -  abstract class Reader extends scala.util.parsing.input.Reader[Token]
    1.87 -
    1.88 -  private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
    1.89 -  {
    1.90 -    def first = tokens.head
    1.91 -    def rest = new Token_Reader(tokens.tail, pos.advance(first))
    1.92 -    def atEnd = tokens.isEmpty
    1.93 -  }
    1.94 -
    1.95 -  def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
    1.96 -}
    1.97 -