--- 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 */
--- 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)