diff -r 9d31fe4ecaea -r aaa984499d36 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sun May 24 10:28:04 2020 +0200 +++ b/src/Pure/ML/ml_process.scala Sun May 24 10:36:42 2020 +0200 @@ -92,7 +92,7 @@ ML_Syntax.print_list( ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list) - List("Resources.init_session_base" + + List("Resources.init_session" + " {session_positions = " + print_sessions(sessions_structure.session_positions) + ", session_directories = " + print_table(sessions_structure.dest_session_directories) + ", docs = " + print_list(base.doc_names) +