# HG changeset patch
# User wenzelm
# Date 1505568956 -7200
# Node ID 6019cfb8256cdc7b59784a1fff3c6afe20eb8c08
# Parent  2e580fcf652236962bc8c8509d85e9d1baa9966e
proper standard_path to revert platform_path in JEdit_Sessions.session_base;

diff -r 2e580fcf6522 -r 6019cfb8256c src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Sep 15 19:56:23 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Sep 16 15:35:56 2017 +0200
@@ -316,11 +316,14 @@
     Symbol.encode_yxml(list(pair(string, string))(table))
   }
 
-  def session_base(resources: Resources): Unit =
+  def session_base(resources: Resources)
+  {
+    val base = resources.session_base.standard_path
     protocol_command("Prover.session_base",
-      encode_table(resources.session_base.global_theories.toList),
-      encode_table(resources.session_base.loaded_theories.toList),
-      encode_table(resources.session_base.dest_known_theories))
+      encode_table(base.global_theories.toList),
+      encode_table(base.loaded_theories.toList),
+      encode_table(base.dest_known_theories))
+  }
 
 
   /* interned items */
diff -r 2e580fcf6522 -r 6019cfb8256c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 15 19:56:23 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Sep 16 15:35:56 2017 +0200
@@ -81,6 +81,11 @@
         theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
         files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
 
+    def standard_path: Known =
+      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))),
+        theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
+        files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
+
     def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
     {
       val res = files.getOrElse(File.canonical(file), Nil).headOption
@@ -114,6 +119,7 @@
     def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
 
     def platform_path: Base = copy(known = known.platform_path)
+    def standard_path: Base = copy(known = known.standard_path)
 
     def loaded_theory(name: Document.Node.Name): Boolean =
       loaded_theories.isDefinedAt(name.theory)