src/Pure/Thy/thy_header.scala
changeset 43611 21a57a0c5f25
parent 41535 0112f14d75ec
child 43646 598b2c6ce13f
     1.1 --- a/src/Pure/Thy/thy_header.scala	Thu Jun 30 16:50:26 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Jun 30 19:24:09 2011 +0200
     1.3 @@ -7,8 +7,9 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.annotation.tailrec
     1.8  import scala.collection.mutable
     1.9 -import scala.util.parsing.input.{Reader, CharSequenceReader}
    1.10 +import scala.util.parsing.input.Reader
    1.11  import scala.util.matching.Regex
    1.12  
    1.13  import java.io.File
    1.14 @@ -25,6 +26,12 @@
    1.15    val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
    1.16  
    1.17    final case class Header(val name: String, val imports: List[String], val uses: List[String])
    1.18 +  {
    1.19 +    def decode_permissive_utf8: Header =
    1.20 +      Header(Standard_System.decode_permissive_utf8(name),
    1.21 +        imports.map(Standard_System.decode_permissive_utf8),
    1.22 +        uses.map(Standard_System.decode_permissive_utf8))
    1.23 +  }
    1.24  
    1.25  
    1.26    /* file name */
    1.27 @@ -50,8 +57,8 @@
    1.28  
    1.29    val header: Parser[Header] =
    1.30    {
    1.31 -    val file_name = atom("file name", _.is_name) ^^ Standard_System.decode_permissive_utf8
    1.32 -    val theory_name = atom("theory name", _.is_name) ^^ Standard_System.decode_permissive_utf8
    1.33 +    val file_name = atom("file name", _.is_name)
    1.34 +    val theory_name = atom("theory name", _.is_name)
    1.35  
    1.36      val file =
    1.37        keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name
    1.38 @@ -70,27 +77,32 @@
    1.39  
    1.40    /* read -- lazy scanning */
    1.41  
    1.42 -  def read(file: File): Header =
    1.43 +  def read(reader: Reader[Char]): Header =
    1.44    {
    1.45      val token = lexicon.token(symbols, _ => false)
    1.46      val toks = new mutable.ListBuffer[Token]
    1.47  
    1.48 -    def scan_to_begin(in: Reader[Char])
    1.49 +    @tailrec def scan_to_begin(in: Reader[Char])
    1.50      {
    1.51        token(in) match {
    1.52          case lexicon.Success(tok, rest) =>
    1.53            toks += tok
    1.54 -          if (!(tok.kind == Token.Kind.KEYWORD && tok.content == BEGIN))
    1.55 -            scan_to_begin(rest)
    1.56 +          if (!tok.is_begin) scan_to_begin(rest)
    1.57          case _ =>
    1.58        }
    1.59      }
    1.60 -    val reader = Scan.byte_reader(file)
    1.61 -    try { scan_to_begin(reader) } finally { reader.close }
    1.62 +    scan_to_begin(reader)
    1.63  
    1.64      parse(commit(header), Token.reader(toks.toList)) match {
    1.65        case Success(result, _) => result
    1.66        case bad => error(bad.toString)
    1.67      }
    1.68    }
    1.69 +
    1.70 +  def read(file: File): Header =
    1.71 +  {
    1.72 +    val reader = Scan.byte_reader(file)
    1.73 +    try { read(reader).decode_permissive_utf8 }
    1.74 +    finally { reader.close }
    1.75 +  }
    1.76  }