src/Pure/ML/ml_process.scala
changeset 72620 429afd0d1a79
parent 72617 5fc193537b7c
child 72628 5e616a454b23
--- a/src/Pure/ML/ml_process.scala	Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/ML/ml_process.scala	Mon Nov 16 13:11:15 2020 +0100
@@ -85,6 +85,9 @@
       session_base match {
         case None => ""
         case Some(base) =>
+          def print_symbols: List[(String, Int)] => String =
+            ML_Syntax.print_list(
+              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_int))
           def print_table: List[(String, String)] => String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
@@ -100,7 +103,8 @@
                 ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
 
           "Resources.init_session" +
-            "{session_positions = " + print_sessions(sessions_structure.session_positions) +
+            "{html_symbols = " + print_symbols(Symbol.codes) +
+            ", session_positions = " + print_sessions(sessions_structure.session_positions) +
             ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
             ", session_chapters = " + print_table(sessions_structure.session_chapters) +
             ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) +