1 /* Title: Pure/Thy/thy_header.scala
4 Static theory header information.
10 import scala.annotation.tailrec
11 import scala.collection.mutable
12 import scala.util.parsing.input.{Reader, CharSequenceReader}
13 import scala.util.matching.Regex
15 import java.io.{File => JFile}
18 object Thy_Header extends Parse.Parser
22 val IMPORTS = "imports"
23 val KEYWORDS = "keywords"
29 Scan.Lexicon("%", "(", ")", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
32 /* theory file name */
34 private val Base_Name = new Regex(""".*?([^/\\:]+)""")
35 private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
37 def base_name(s: String): String =
38 s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
40 def thy_name(s: String): Option[String] =
41 s match { case Thy_Name(name) => Some(name) case _ => None }
46 val header: Parser[Thy_Header] =
48 val file_name = atom("file name", _.is_name)
49 val theory_name = atom("theory name", _.is_name)
52 atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
54 rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
55 { case xs ~ y => xs.map((_, y)) }
57 keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
58 { case xs ~ yss => (xs :: yss).flatten }
61 keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
62 file_name ^^ (x => (x, true))
66 (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
67 (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
68 (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
70 { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
72 (keyword(HEADER) ~ tags) ~!
73 ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
74 (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
78 /* read -- lazy scanning */
80 def read(reader: Reader[Char]): Thy_Header =
82 val token = lexicon.token(_ => false)
83 val toks = new mutable.ListBuffer[Token]
85 @tailrec def scan_to_begin(in: Reader[Char])
88 case lexicon.Success(tok, rest) =>
90 if (!tok.is_begin) scan_to_begin(rest)
96 parse(commit(header), Token.reader(toks.toList)) match {
97 case Success(result, _) => result
98 case bad => error(bad.toString)
102 def read(source: CharSequence): Thy_Header =
103 read(new CharSequenceReader(source))
105 def read(file: JFile): Thy_Header =
107 val reader = Scan.byte_reader(file)
108 try { read(reader).map(Standard_System.decode_permissive_utf8) }
109 finally { reader.close }
114 sealed case class Thy_Header(
115 name: String, imports: List[String],
116 keywords: List[Outer_Syntax.Decl],
117 uses: List[(String, Boolean)])
119 def map(f: String => String): Thy_Header =
120 Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2)))