tuned signature;
authorwenzelm
Fri Sep 29 17:41:39 2017 +0200 (21 months ago)
changeset 667168737b866bd1c
parent 66715 6bced18e2b91
child 66717 67dbf5cdc056
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Sep 29 17:35:09 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Sep 29 17:41:39 2017 +0200
     1.3 @@ -116,6 +116,8 @@
     1.4            case _ => false
     1.5          }
     1.6  
     1.7 +      def path: Path = Path.explode(node)
     1.8 +
     1.9        def is_theory: Boolean = theory.nonEmpty
    1.10  
    1.11        def theory_base_name: String = Long_Name.base_name(theory)
     2.1 --- a/src/Pure/PIDE/resources.scala	Fri Sep 29 17:35:09 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Fri Sep 29 17:41:39 2017 +0200
     2.3 @@ -117,7 +117,7 @@
     2.4  
     2.5    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
     2.6    {
     2.7 -    val path = File.check_file(Path.explode(name.node))
     2.8 +    val path = File.check_file(name.path)
     2.9      val reader = Scan.byte_reader(path.file)
    2.10      try { f(reader) } finally { reader.close }
    2.11    }
     3.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 17:35:09 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 17:41:39 2017 +0200
     3.3 @@ -40,8 +40,7 @@
     3.4        def local_theories_iterator =
     3.5        {
     3.6          val local_path = local_dir.canonical_file.toPath
     3.7 -        theories.iterator.filter(name =>
     3.8 -          Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
     3.9 +        theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
    3.10        }
    3.11  
    3.12        val known_theories =
    3.13 @@ -62,7 +61,7 @@
    3.14          (Map.empty[JFile, List[Document.Node.Name]] /:
    3.15              (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
    3.16            case (known, name) =>
    3.17 -            val file = Path.explode(name.node).canonical_file
    3.18 +            val file = name.path.canonical_file
    3.19              val theories1 = known.getOrElse(file, Nil)
    3.20              if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
    3.21                known
    3.22 @@ -205,7 +204,7 @@
    3.23  
    3.24              val syntax = thy_deps.syntax
    3.25  
    3.26 -            val theory_files = thy_deps.names.map(name => Path.explode(name.node))
    3.27 +            val theory_files = thy_deps.names.map(_.path)
    3.28              val loaded_files =
    3.29                if (inlined_files) {
    3.30                  if (Sessions.is_pure(info.name)) {
     4.1 --- a/src/Pure/Tools/imports.scala	Fri Sep 29 17:35:09 2017 +0200
     4.2 +++ b/src/Pure/Tools/imports.scala	Fri Sep 29 17:41:39 2017 +0200
     4.3 @@ -105,7 +105,7 @@
     4.4            (for {
     4.5              (_, a) <- session_resources.session_base.known.theories.iterator
     4.6              if session_resources.theory_qualifier(a) == info.theory_qualifier
     4.7 -            b <- deps.all_known.get_file(Path.explode(a.node).file)
     4.8 +            b <- deps.all_known.get_file(a.path.file)
     4.9              qualifier = session_resources.theory_qualifier(b)
    4.10              if !declared_imports.contains(qualifier)
    4.11            } yield qualifier).toSet
    4.12 @@ -146,7 +146,7 @@
    4.13              val s1 =
    4.14                if (imports_base.loaded_theory(name)) name.theory
    4.15                else {
    4.16 -                imports_base.known.get_file(Path.explode(name.node).file) match {
    4.17 +                imports_base.known.get_file(name.path.file) match {
    4.18                    case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    4.19                      name1.theory
    4.20                    case Some(name1) if Thy_Header.is_base_name(s) =>