src/Pure/Thy/sessions.scala
changeset 66716 8737b866bd1c
parent 66715 6bced18e2b91
child 66717 67dbf5cdc056
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 17:35:09 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 17:41:39 2017 +0200
     1.3 @@ -40,8 +40,7 @@
     1.4        def local_theories_iterator =
     1.5        {
     1.6          val local_path = local_dir.canonical_file.toPath
     1.7 -        theories.iterator.filter(name =>
     1.8 -          Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
     1.9 +        theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
    1.10        }
    1.11  
    1.12        val known_theories =
    1.13 @@ -62,7 +61,7 @@
    1.14          (Map.empty[JFile, List[Document.Node.Name]] /:
    1.15              (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
    1.16            case (known, name) =>
    1.17 -            val file = Path.explode(name.node).canonical_file
    1.18 +            val file = name.path.canonical_file
    1.19              val theories1 = known.getOrElse(file, Nil)
    1.20              if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
    1.21                known
    1.22 @@ -205,7 +204,7 @@
    1.23  
    1.24              val syntax = thy_deps.syntax
    1.25  
    1.26 -            val theory_files = thy_deps.names.map(name => Path.explode(name.node))
    1.27 +            val theory_files = thy_deps.names.map(_.path)
    1.28              val loaded_files =
    1.29                if (inlined_files) {
    1.30                  if (Sessions.is_pure(info.name)) {