more general theory header parsing;
authorwenzelm
Thu Jun 30 19:24:09 2011 +0200 (2011-06-30)
changeset 4361121a57a0c5f25
parent 43610 16482dc641d4
child 43617 5e22da27b5fa
more general theory header parsing;
src/Pure/Isar/token.scala
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Isar/token.scala	Thu Jun 30 16:50:26 2011 +0200
     1.2 +++ b/src/Pure/Isar/token.scala	Thu Jun 30 19:24:09 2011 +0200
     1.3 @@ -81,6 +81,9 @@
     1.4    def is_comment: Boolean = kind == Token.Kind.COMMENT
     1.5    def is_ignored: Boolean = is_space || is_comment
     1.6  
     1.7 +  def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
     1.8 +  def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
     1.9 +
    1.10    def content: String =
    1.11      if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
    1.12      else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
     2.1 --- a/src/Pure/Thy/thy_header.scala	Thu Jun 30 16:50:26 2011 +0200
     2.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Jun 30 19:24:09 2011 +0200
     2.3 @@ -7,8 +7,9 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import scala.annotation.tailrec
     2.8  import scala.collection.mutable
     2.9 -import scala.util.parsing.input.{Reader, CharSequenceReader}
    2.10 +import scala.util.parsing.input.Reader
    2.11  import scala.util.matching.Regex
    2.12  
    2.13  import java.io.File
    2.14 @@ -25,6 +26,12 @@
    2.15    val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
    2.16  
    2.17    final case class Header(val name: String, val imports: List[String], val uses: List[String])
    2.18 +  {
    2.19 +    def decode_permissive_utf8: Header =
    2.20 +      Header(Standard_System.decode_permissive_utf8(name),
    2.21 +        imports.map(Standard_System.decode_permissive_utf8),
    2.22 +        uses.map(Standard_System.decode_permissive_utf8))
    2.23 +  }
    2.24  
    2.25  
    2.26    /* file name */
    2.27 @@ -50,8 +57,8 @@
    2.28  
    2.29    val header: Parser[Header] =
    2.30    {
    2.31 -    val file_name = atom("file name", _.is_name) ^^ Standard_System.decode_permissive_utf8
    2.32 -    val theory_name = atom("theory name", _.is_name) ^^ Standard_System.decode_permissive_utf8
    2.33 +    val file_name = atom("file name", _.is_name)
    2.34 +    val theory_name = atom("theory name", _.is_name)
    2.35  
    2.36      val file =
    2.37        keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name
    2.38 @@ -70,27 +77,32 @@
    2.39  
    2.40    /* read -- lazy scanning */
    2.41  
    2.42 -  def read(file: File): Header =
    2.43 +  def read(reader: Reader[Char]): Header =
    2.44    {
    2.45      val token = lexicon.token(symbols, _ => false)
    2.46      val toks = new mutable.ListBuffer[Token]
    2.47  
    2.48 -    def scan_to_begin(in: Reader[Char])
    2.49 +    @tailrec def scan_to_begin(in: Reader[Char])
    2.50      {
    2.51        token(in) match {
    2.52          case lexicon.Success(tok, rest) =>
    2.53            toks += tok
    2.54 -          if (!(tok.kind == Token.Kind.KEYWORD && tok.content == BEGIN))
    2.55 -            scan_to_begin(rest)
    2.56 +          if (!tok.is_begin) scan_to_begin(rest)
    2.57          case _ =>
    2.58        }
    2.59      }
    2.60 -    val reader = Scan.byte_reader(file)
    2.61 -    try { scan_to_begin(reader) } finally { reader.close }
    2.62 +    scan_to_begin(reader)
    2.63  
    2.64      parse(commit(header), Token.reader(toks.toList)) match {
    2.65        case Success(result, _) => result
    2.66        case bad => error(bad.toString)
    2.67      }
    2.68    }
    2.69 +
    2.70 +  def read(file: File): Header =
    2.71 +  {
    2.72 +    val reader = Scan.byte_reader(file)
    2.73 +    try { read(reader).decode_permissive_utf8 }
    2.74 +    finally { reader.close }
    2.75 +  }
    2.76  }