src/Pure/Tools/ml_process.scala
changeset 65441 9425e4d8bdb6
parent 65432 d938705819bb
child 65457 2bf0d2fcd506
--- a/src/Pure/Tools/ml_process.scala	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Sat Apr 08 20:56:41 2017 +0200
@@ -95,10 +95,15 @@
       session_base match {
         case None => Nil
         case Some(base) =>
-          List("Resources.set_session_base {known_theories = " +
+          def print_table(table: List[(String, String)]): String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
-                ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
+                ML_Syntax.print_string, ML_Syntax.print_string))(table)
+          List("Resources.set_session_base {default_qualifier = \"\"" +
+            ", global_theories = " +
+              ML_Syntax.print_list(ML_Syntax.print_string)(base.global_theories.toList) +
+            ", loaded_theories = " + print_table(base.dest_loaded_theories) +
+            ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }
 
     // process