# HG changeset patch
# User wenzelm
# Date 1605565036 -3600
# Node ID 3402df4486de33401034f4a1bbb5d29a60693562
# Parent  35524fade6a4b0bd1c8d4446a2e71c718f19dfbd
proper html_symbols (amending 429afd0d1a79);

diff -r 35524fade6a4 -r 3402df4486de src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Nov 16 22:46:02 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Nov 16 23:17:16 2020 +0100
@@ -289,6 +289,8 @@
   {
     import XML.Encode._
 
+    def encode_symbols(arg: List[(String, Int)]): String =
+      Symbol.encode_yxml(list(pair(string, int))(arg))
     def encode_table(arg: List[(String, String)]): String =
       Symbol.encode_yxml(list(pair(string, string))(arg))
     def encode_list(arg: List[String]): String =
@@ -299,6 +301,7 @@
       Symbol.encode_yxml(list(pair(string, list(string)))(arg))
 
     protocol_command("Prover.init_session",
+      encode_symbols(Symbol.codes),
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),
       encode_table(resources.sessions_structure.session_chapters),