tuned signature;
authorwenzelm
Wed Mar 15 10:08:27 2017 +0100 (2017-03-15)
changeset 6525013a6c81534a8
parent 65249 c3ee88b9c3cb
child 65251 4b0a43afc3fb
tuned signature;
src/Pure/PIDE/resources.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Tue Mar 14 23:25:53 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Mar 15 10:08:27 2017 +0100
     1.3 @@ -15,8 +15,6 @@
     1.4  
     1.5  object Resources
     1.6  {
     1.7 -  def thy_path(path: Path): Path = path.ext("thy")
     1.8 -
     1.9    val empty: Resources = new Resources(Sessions.Base.empty)
    1.10  }
    1.11  
    1.12 @@ -24,6 +22,8 @@
    1.13  {
    1.14    val thy_info = new Thy_Info(this)
    1.15  
    1.16 +  def thy_path(path: Path): Path = path.ext("thy")
    1.17 +
    1.18  
    1.19    /* document node names */
    1.20  
    1.21 @@ -100,7 +100,7 @@
    1.22          val theory = path.base.implode
    1.23          if (Long_Name.is_qualified(theory)) dummy_name(theory)
    1.24          else {
    1.25 -          val node = append(master.master_dir, Resources.thy_path(path))
    1.26 +          val node = append(master.master_dir, thy_path(path))
    1.27            val master_dir = append(master.master_dir, path.dir)
    1.28            Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, theory))
    1.29          }
    1.30 @@ -128,7 +128,7 @@
    1.31          val (name, pos) = header.name
    1.32          if (base_name != name)
    1.33            error("Bad theory name " + quote(name) +
    1.34 -            " for file " + Resources.thy_path(Path.basic(base_name)) + Position.here(pos) +
    1.35 +            " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
    1.36              Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    1.37  
    1.38          val imports =
     2.1 --- a/src/Pure/Tools/build.scala	Tue Mar 14 23:25:53 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 15 10:08:27 2017 +0100
     2.3 @@ -135,7 +135,7 @@
     2.4                    case (global, _, thys) =>
     2.5                      thys.map(thy =>
     2.6                        (resources.node_name(
     2.7 -                        if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos))
     2.8 +                        if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
     2.9                  })
    2.10                val thy_deps = resources.thy_info.dependencies(name, root_theories)
    2.11