# HG changeset patch
# User wenzelm
# Date 1314877180 -7200
# Node ID 4beeaf2a226d74777fcf77f1141b3d2a0b2e3c81
# Parent  a4ff8a7872025a18633cca7fe7a3cbe1b6c58ba0
tuned signature;

diff -r a4ff8a787202 -r 4beeaf2a226d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Sep 01 13:34:45 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Sep 01 13:39:40 2011 +0200
@@ -39,7 +39,7 @@
 
   object Node
   {
-    sealed case class Name(node: String, master_dir: String, theory: String)
+    sealed case class Name(node: String, dir: String, theory: String)
     {
       override def hashCode: Int = node.hashCode
       override def equals(that: Any): Boolean =
diff -r a4ff8a787202 -r 4beeaf2a226d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Sep 01 13:34:45 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Sep 01 13:39:40 2011 +0200
@@ -146,10 +146,9 @@
     {
       val thy_name = Thy_Header.base_name(s)
       if (thy_load.is_loaded(thy_name)) thy_name
-      else thy_load.append(name.master_dir, Thy_Header.thy_path(Path.explode(s)))
+      else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
     }
-    def norm_use(s: String): String =
-      thy_load.append(name.master_dir, Path.explode(s))
+    def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
 
     val header1: Document.Node_Header =
       header match {
diff -r a4ff8a787202 -r 4beeaf2a226d src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Thu Sep 01 13:34:45 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Thu Sep 01 13:39:40 2011 +0200
@@ -38,12 +38,13 @@
 
   /* dependencies */
 
-  def import_name(master_dir: String, str: String): Document.Node.Name =
+  def import_name(dir: String, str: String): Document.Node.Name =
   {
     val path = Path.explode(str)
-    val node_name = thy_load.append(master_dir, Thy_Header.thy_path(path))
-    val master_dir1 = thy_load.append(master_dir, path.dir)
-    Document.Node.Name(node_name, master_dir1, path.base.implode)
+    val node = thy_load.append(dir, Thy_Header.thy_path(path))
+    val dir1 = thy_load.append(dir, path.dir)
+    val theory = path.base.implode
+    Document.Node.Name(node, dir1, theory)
   }
 
   type Deps = Map[Document.Node.Name, Document.Node_Header]
@@ -66,7 +67,7 @@
               cat_error(msg, "The error(s) above occurred while examining theory " +
                 quote(name.theory) + required_by(initiators))
           }
-        val imports = header.imports.map(import_name(name.master_dir, _))
+        val imports = header.imports.map(import_name(name.dir, _))
         require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports)
       }
       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
diff -r a4ff8a787202 -r 4beeaf2a226d src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Thu Sep 01 13:34:45 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala	Thu Sep 01 13:39:40 2011 +0200
@@ -10,7 +10,7 @@
 {
   def register_thy(thy_name: String)
   def is_loaded(thy_name: String): Boolean
-  def append(master_dir: String, path: Path): String
+  def append(dir: String, path: Path): String
   def check_thy(node_name: Document.Node.Name): Thy_Header
 }