# HG changeset patch # User wenzelm # Date 1261514897 -3600 # Node ID 7501b2910900dd98286863b19400a9b535006efe # Parent 18843829c7f2579a2296225c134193e8e5b1f599 basic setup for header scanning/parsing; diff -r 18843829c7f2 -r 7501b2910900 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Tue Dec 22 21:47:27 2009 +0100 +++ b/src/Pure/Thy/thy_header.scala Tue Dec 22 21:48:17 2009 +0100 @@ -1,12 +1,16 @@ /* Title: Pure/Thy/thy_header.scala Author: Makarius -Theory header keywords. +Theory headers -- independent of outer syntax. */ package isabelle +import scala.collection.mutable +import scala.util.parsing.input.{Reader, CharSequenceReader} + + object Thy_Header { val HEADER = "header" @@ -15,5 +19,54 @@ val USES = "uses" val BEGIN = "begin" - val keywords = List("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES) + val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES) } + + +class Thy_Header(symbols: Symbol.Interpretation) extends Outer_Parse.Parser +{ + import Thy_Header._ + + + /* header */ + + val header: Parser[(String, List[String], List[String])] = + { + val file_name = atom("file name", _.is_name) + val theory_name = atom("theory name", _.is_name) + + val file = + keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name + + val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs } + + val args = + theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^ + { case x ~ (_ ~ (ys ~ zs ~ _)) => (x, ys, zs) } + + (keyword(HEADER) ~ tags) ~! + ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } | + (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } + } + + + /* scan -- lazy approximation */ + + def scan(text: CharSequence): List[Outer_Lex.Token] = + { + val token = lexicon.token(symbols, _ => false) + val toks = new mutable.ListBuffer[Outer_Lex.Token] + def scan_until_begin(in: Reader[Char]) + { + token(in) match { + case lexicon.Success(tok, rest) => + toks += tok + if (!(tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == BEGIN)) + scan_until_begin(rest) + case _ => + } + } + scan_until_begin(new CharSequenceReader(text)) + toks.toList + } +}