tuned signature;
authorwenzelm
Thu Sep 01 13:39:40 2011 +0200 (2011-09-01 ago)
changeset 446164beeaf2a226d
parent 44615 a4ff8a787202
child 44617 5db68864a967
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Sep 01 13:34:45 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Sep 01 13:39:40 2011 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4  
     1.5    object Node
     1.6    {
     1.7 -    sealed case class Name(node: String, master_dir: String, theory: String)
     1.8 +    sealed case class Name(node: String, dir: String, theory: String)
     1.9      {
    1.10        override def hashCode: Int = node.hashCode
    1.11        override def equals(that: Any): Boolean =
     2.1 --- a/src/Pure/System/session.scala	Thu Sep 01 13:34:45 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Thu Sep 01 13:39:40 2011 +0200
     2.3 @@ -146,10 +146,9 @@
     2.4      {
     2.5        val thy_name = Thy_Header.base_name(s)
     2.6        if (thy_load.is_loaded(thy_name)) thy_name
     2.7 -      else thy_load.append(name.master_dir, Thy_Header.thy_path(Path.explode(s)))
     2.8 +      else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
     2.9      }
    2.10 -    def norm_use(s: String): String =
    2.11 -      thy_load.append(name.master_dir, Path.explode(s))
    2.12 +    def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
    2.13  
    2.14      val header1: Document.Node_Header =
    2.15        header match {
     3.1 --- a/src/Pure/Thy/thy_info.scala	Thu Sep 01 13:34:45 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.scala	Thu Sep 01 13:39:40 2011 +0200
     3.3 @@ -38,12 +38,13 @@
     3.4  
     3.5    /* dependencies */
     3.6  
     3.7 -  def import_name(master_dir: String, str: String): Document.Node.Name =
     3.8 +  def import_name(dir: String, str: String): Document.Node.Name =
     3.9    {
    3.10      val path = Path.explode(str)
    3.11 -    val node_name = thy_load.append(master_dir, Thy_Header.thy_path(path))
    3.12 -    val master_dir1 = thy_load.append(master_dir, path.dir)
    3.13 -    Document.Node.Name(node_name, master_dir1, path.base.implode)
    3.14 +    val node = thy_load.append(dir, Thy_Header.thy_path(path))
    3.15 +    val dir1 = thy_load.append(dir, path.dir)
    3.16 +    val theory = path.base.implode
    3.17 +    Document.Node.Name(node, dir1, theory)
    3.18    }
    3.19  
    3.20    type Deps = Map[Document.Node.Name, Document.Node_Header]
    3.21 @@ -66,7 +67,7 @@
    3.22                cat_error(msg, "The error(s) above occurred while examining theory " +
    3.23                  quote(name.theory) + required_by(initiators))
    3.24            }
    3.25 -        val imports = header.imports.map(import_name(name.master_dir, _))
    3.26 +        val imports = header.imports.map(import_name(name.dir, _))
    3.27          require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports)
    3.28        }
    3.29        catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
     4.1 --- a/src/Pure/Thy/thy_load.scala	Thu Sep 01 13:34:45 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_load.scala	Thu Sep 01 13:39:40 2011 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4  {
     4.5    def register_thy(thy_name: String)
     4.6    def is_loaded(thy_name: String): Boolean
     4.7 -  def append(master_dir: String, path: Path): String
     4.8 +  def append(dir: String, path: Path): String
     4.9    def check_thy(node_name: Document.Node.Name): Thy_Header
    4.10  }
    4.11