# HG changeset patch
# User wenzelm
# Date 1568657185 -7200
# Node ID fb94d68314fad042bdb9ed0f1d0a1521097a25c5
# Parent  530b575d8cffa9cdd661ad3ea87c4f78f5c19729
clarified signature -- removed pointless operations;

diff -r 530b575d8cff -r fb94d68314fa src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Sep 16 19:48:09 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Sep 16 20:06:25 2019 +0200
@@ -239,13 +239,12 @@
 
   def session_base(resources: Resources)
   {
-    val base = resources.session_base.standard_path
     protocol_command("Prover.init_session_base",
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),
-      encode_list(base.doc_names),
-      encode_table(base.global_theories.toList),
-      encode_list(base.loaded_theories.keys))
+      encode_list(resources.session_base.doc_names),
+      encode_table(resources.session_base.global_theories.toList),
+      encode_list(resources.session_base.loaded_theories.keys))
   }
 
 
diff -r 530b575d8cff -r fb94d68314fa src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 16 19:48:09 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 16 20:06:25 2019 +0200
@@ -110,9 +110,6 @@
       "Sessions.Base(loaded_theories = " + loaded_theories.size +
         ", used_theories = " + used_theories.length + ")"
 
-    def platform_path: Base = copy(known = known.platform_path)
-    def standard_path: Base = copy(known = known.standard_path)
-
     def theory_qualifier(name: String): String =
       global_theories.getOrElse(name, Long_Name.qualifier(name))
     def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
diff -r 530b575d8cff -r fb94d68314fa src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Sep 16 19:48:09 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Sep 16 20:06:25 2019 +0200
@@ -28,7 +28,7 @@
 }
 
 class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
-  extends Resources(session_base_info.sessions_structure, session_base_info.base.platform_path)
+  extends Resources(session_base_info.sessions_structure, session_base_info.base)
 {
   def session_name: String = session_base_info.session
   def session_errors: List[String] = session_base_info.errors