# HG changeset patch
# User wenzelm
# Date 1506699699 -7200
# Node ID 8737b866bd1ce5890d1e29c35ad932bcfb6c0b86
# Parent  6bced18e2b919b469b3367af00ff671710afc502
tuned signature;

diff -r 6bced18e2b91 -r 8737b866bd1c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Sep 29 17:35:09 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Sep 29 17:41:39 2017 +0200
@@ -116,6 +116,8 @@
           case _ => false
         }
 
+      def path: Path = Path.explode(node)
+
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
diff -r 6bced18e2b91 -r 8737b866bd1c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Sep 29 17:35:09 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Sep 29 17:41:39 2017 +0200
@@ -117,7 +117,7 @@
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
-    val path = File.check_file(Path.explode(name.node))
+    val path = File.check_file(name.path)
     val reader = Scan.byte_reader(path.file)
     try { f(reader) } finally { reader.close }
   }
diff -r 6bced18e2b91 -r 8737b866bd1c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 29 17:35:09 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 17:41:39 2017 +0200
@@ -40,8 +40,7 @@
       def local_theories_iterator =
       {
         val local_path = local_dir.canonical_file.toPath
-        theories.iterator.filter(name =>
-          Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
+        theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
       }
 
       val known_theories =
@@ -62,7 +61,7 @@
         (Map.empty[JFile, List[Document.Node.Name]] /:
             (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
           case (known, name) =>
-            val file = Path.explode(name.node).canonical_file
+            val file = name.path.canonical_file
             val theories1 = known.getOrElse(file, Nil)
             if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
               known
@@ -205,7 +204,7 @@
 
             val syntax = thy_deps.syntax
 
-            val theory_files = thy_deps.names.map(name => Path.explode(name.node))
+            val theory_files = thy_deps.names.map(_.path)
             val loaded_files =
               if (inlined_files) {
                 if (Sessions.is_pure(info.name)) {
diff -r 6bced18e2b91 -r 8737b866bd1c src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Fri Sep 29 17:35:09 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Fri Sep 29 17:41:39 2017 +0200
@@ -105,7 +105,7 @@
           (for {
             (_, a) <- session_resources.session_base.known.theories.iterator
             if session_resources.theory_qualifier(a) == info.theory_qualifier
-            b <- deps.all_known.get_file(Path.explode(a.node).file)
+            b <- deps.all_known.get_file(a.path.file)
             qualifier = session_resources.theory_qualifier(b)
             if !declared_imports.contains(qualifier)
           } yield qualifier).toSet
@@ -146,7 +146,7 @@
             val s1 =
               if (imports_base.loaded_theory(name)) name.theory
               else {
-                imports_base.known.get_file(Path.explode(name.node).file) match {
+                imports_base.known.get_file(name.path.file) match {
                   case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
                     name1.theory
                   case Some(name1) if Thy_Header.is_base_name(s) =>