--- a/src/Pure/Thy/thy_header.scala Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala Fri Aug 12 12:03:17 2011 +0200
@@ -25,12 +25,6 @@
val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
- sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
- {
- def map(f: String => String): Header =
- Header(f(name), imports.map(f), uses.map(f))
- }
-
/* file name */
@@ -45,7 +39,7 @@
/* header */
- val header: Parser[Header] =
+ val header: Parser[Thy_Header] =
{
val file_name = atom("file name", _.is_name)
val theory_name = atom("theory name", _.is_name)
@@ -57,7 +51,7 @@
val args =
theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
- { case x ~ (_ ~ (ys ~ zs ~ _)) => Header(x, ys, zs) }
+ { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
(keyword(HEADER) ~ tags) ~!
((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
@@ -67,7 +61,7 @@
/* read -- lazy scanning */
- def read(reader: Reader[Char]): Header =
+ def read(reader: Reader[Char]): Thy_Header =
{
val token = lexicon.token(_ => false)
val toks = new mutable.ListBuffer[Token]
@@ -89,10 +83,10 @@
}
}
- def read(source: CharSequence): Header =
+ def read(source: CharSequence): Thy_Header =
read(new CharSequenceReader(source))
- def read(file: File): Header =
+ def read(file: File): Thy_Header =
{
val reader = Scan.byte_reader(file)
try { read(reader).map(Standard_System.decode_permissive_utf8) }
@@ -102,7 +96,7 @@
/* check */
- def check(name: String, source: CharSequence): Header =
+ def check(name: String, source: CharSequence): Thy_Header =
{
val header = read(source)
val name1 = header.name
@@ -111,3 +105,11 @@
header
}
}
+
+
+sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
+{
+ def map(f: String => String): Thy_Header =
+ Thy_Header(f(name), imports.map(f), uses.map(f))
+}
+