src/Pure/PIDE/resources.scala
changeset 65250 13a6c81534a8
parent 64856 5e9bf964510a
child 65255 d388e63a46fc
     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 =