# HG changeset patch
# User wenzelm
# Date 1605458555 -3600
# Node ID ffed574c65c385acc23a205f1d350fc5d049bbac
# Parent  d01ea9e3bd2da9a8bd478a2b0f3477c4a2ed5f86
tuned;

diff -r d01ea9e3bd2d -r ffed574c65c3 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sun Nov 15 17:34:19 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Sun Nov 15 17:42:35 2020 +0100
@@ -86,15 +86,15 @@
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
                 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
-          def print_list(list: List[String]): String =
-            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
-          def print_sessions(list: List[(String, Position.T)]): String =
+          def print_list: List[String] => String =
+            ML_Syntax.print_list(ML_Syntax.print_string_bytes)
+          def print_sessions: List[(String, Position.T)] => String =
             ML_Syntax.print_list(
-              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
-          def print_bibtex_entries(list: List[(String, List[String])]): String =
+              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))
+          def print_bibtex_entries: List[(String, List[String])] => String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes,
-                ML_Syntax.print_list(ML_Syntax.print_string_bytes)))(list)
+                ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
 
           List("Resources.init_session" +
             "{session_positions = " + print_sessions(sessions_structure.session_positions) +
diff -r d01ea9e3bd2d -r ffed574c65c3 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Nov 15 17:34:19 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sun Nov 15 17:42:35 2020 +0100
@@ -285,32 +285,19 @@
 
   /* session base */
 
-  private def encode_table(table: List[(String, String)]): String =
-  {
-    import XML.Encode._
-    Symbol.encode_yxml(list(pair(string, string))(table))
-  }
-
-  private def encode_list(lst: List[String]): String =
+  def init_session(resources: Resources)
   {
     import XML.Encode._
-    Symbol.encode_yxml(list(string)(lst))
-  }
-
-  private def encode_sessions(lst: List[(String, Position.T)]): String =
-  {
-    import XML.Encode._
-    Symbol.encode_yxml(list(pair(string, properties))(lst))
-  }
 
-  private def encode_bibtex_entries(lst: List[(String, List[String])]): String =
-  {
-    import XML.Encode._
-    Symbol.encode_yxml(list(pair(string, list(string)))(lst))
-  }
+    def encode_table(arg: List[(String, String)]): String =
+      Symbol.encode_yxml(list(pair(string, string))(arg))
+    def encode_list(arg: List[String]): String =
+      Symbol.encode_yxml(list(string)(arg))
+    def encode_sessions(arg: List[(String, Position.T)]): String =
+      Symbol.encode_yxml(list(pair(string, properties))(arg))
+    def encode_bibtex_entries(arg: List[(String, List[String])]): String =
+      Symbol.encode_yxml(list(pair(string, list(string)))(arg))
 
-  def init_session(resources: Resources)
-  {
     protocol_command("Prover.init_session",
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),