simplified class Thy_Header;
authorwenzelm
Fri Aug 12 12:03:17 2011 +0200 (2011-08-12)
changeset 441599a35e88d9dc9
parent 44158 fe6d1ae7a065
child 44160 8848867501fb
simplified class Thy_Header;
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 12 11:41:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 12 12:03:17 2011 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4      case class Edits[A](edits: List[A]) extends Edit[A]
     1.5      case class Update_Header[A](header: Header) extends Edit[A]
     1.6  
     1.7 -    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
     1.8 +    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header])
     1.9      val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
    1.10  
    1.11      val empty: Node = Node(empty_header, Map(), Linear_Set())
     2.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Aug 12 11:41:26 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 12 12:03:17 2011 +0200
     2.3 @@ -150,7 +150,7 @@
     2.4              { case Document.Node.Remove() => (Nil, Nil) },
     2.5              { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
     2.6              { case Document.Node.Update_Header(
     2.7 -                  Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
     2.8 +                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
     2.9                  (Nil, triple(string, list(string), list(string))(a, b, c)) },
    2.10              { case Document.Node.Update_Header(
    2.11                    Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
     3.1 --- a/src/Pure/System/session.scala	Fri Aug 12 11:41:26 2011 +0200
     3.2 +++ b/src/Pure/System/session.scala	Fri Aug 12 12:03:17 2011 +0200
     3.3 @@ -146,7 +146,7 @@
     3.4      override def is_loaded(name: String): Boolean =
     3.5        loaded_theories.contains(name)
     3.6  
     3.7 -    override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
     3.8 +    override def check_thy(dir: Path, name: String): (String, Thy_Header) =
     3.9      {
    3.10        val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
    3.11        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
     4.1 --- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 11:41:26 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 12:03:17 2011 +0200
     4.3 @@ -25,12 +25,6 @@
     4.4  
     4.5    val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
     4.6  
     4.7 -  sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
     4.8 -  {
     4.9 -    def map(f: String => String): Header =
    4.10 -      Header(f(name), imports.map(f), uses.map(f))
    4.11 -  }
    4.12 -
    4.13  
    4.14    /* file name */
    4.15  
    4.16 @@ -45,7 +39,7 @@
    4.17  
    4.18    /* header */
    4.19  
    4.20 -  val header: Parser[Header] =
    4.21 +  val header: Parser[Thy_Header] =
    4.22    {
    4.23      val file_name = atom("file name", _.is_name)
    4.24      val theory_name = atom("theory name", _.is_name)
    4.25 @@ -57,7 +51,7 @@
    4.26  
    4.27      val args =
    4.28        theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
    4.29 -        { case x ~ (_ ~ (ys ~ zs ~ _)) => Header(x, ys, zs) }
    4.30 +        { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
    4.31  
    4.32      (keyword(HEADER) ~ tags) ~!
    4.33        ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
    4.34 @@ -67,7 +61,7 @@
    4.35  
    4.36    /* read -- lazy scanning */
    4.37  
    4.38 -  def read(reader: Reader[Char]): Header =
    4.39 +  def read(reader: Reader[Char]): Thy_Header =
    4.40    {
    4.41      val token = lexicon.token(_ => false)
    4.42      val toks = new mutable.ListBuffer[Token]
    4.43 @@ -89,10 +83,10 @@
    4.44      }
    4.45    }
    4.46  
    4.47 -  def read(source: CharSequence): Header =
    4.48 +  def read(source: CharSequence): Thy_Header =
    4.49      read(new CharSequenceReader(source))
    4.50  
    4.51 -  def read(file: File): Header =
    4.52 +  def read(file: File): Thy_Header =
    4.53    {
    4.54      val reader = Scan.byte_reader(file)
    4.55      try { read(reader).map(Standard_System.decode_permissive_utf8) }
    4.56 @@ -102,7 +96,7 @@
    4.57  
    4.58    /* check */
    4.59  
    4.60 -  def check(name: String, source: CharSequence): Header =
    4.61 +  def check(name: String, source: CharSequence): Thy_Header =
    4.62    {
    4.63      val header = read(source)
    4.64      val name1 = header.name
    4.65 @@ -111,3 +105,11 @@
    4.66      header
    4.67    }
    4.68  }
    4.69 +
    4.70 +
    4.71 +sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
    4.72 +{
    4.73 +  def map(f: String => String): Thy_Header =
    4.74 +    Thy_Header(f(name), imports.map(f), uses.map(f))
    4.75 +}
    4.76 +
     5.1 --- a/src/Pure/Thy/thy_info.scala	Fri Aug 12 11:41:26 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Aug 12 12:03:17 2011 +0200
     5.3 @@ -38,7 +38,7 @@
     5.4  
     5.5    /* dependencies */
     5.6  
     5.7 -  type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
     5.8 +  type Deps = Map[String, Exn.Result[(String, Thy_Header)]]  // name -> (text, header)
     5.9  
    5.10    private def require_thys(ignored: String => Boolean,
    5.11        initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
     6.1 --- a/src/Pure/Thy/thy_load.scala	Fri Aug 12 11:41:26 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_load.scala	Fri Aug 12 12:03:17 2011 +0200
     6.3 @@ -10,6 +10,6 @@
     6.4  {
     6.5    def is_loaded(name: String): Boolean
     6.6  
     6.7 -  def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
     6.8 +  def check_thy(dir: Path, name: String): (String, Thy_Header)
     6.9  }
    6.10