equal
deleted
inserted
replaced
97 case Some(base) => |
97 case Some(base) => |
98 def print_table(table: List[(String, String)]): String = |
98 def print_table(table: List[(String, String)]): String = |
99 ML_Syntax.print_list( |
99 ML_Syntax.print_list( |
100 ML_Syntax.print_pair( |
100 ML_Syntax.print_pair( |
101 ML_Syntax.print_string, ML_Syntax.print_string))(table) |
101 ML_Syntax.print_string, ML_Syntax.print_string))(table) |
102 List("Resources.init_session_base {default_qualifier = \"\"" + |
102 List("Resources.init_session_base" + |
103 ", global_theories = " + print_table(base.global_theories.toList) + |
103 " {global_theories = " + print_table(base.global_theories.toList) + |
104 ", loaded_theories = " + print_table(base.loaded_theories.toList) + |
104 ", loaded_theories = " + print_table(base.loaded_theories.toList) + |
105 ", known_theories = " + print_table(base.dest_known_theories) + "}") |
105 ", known_theories = " + print_table(base.dest_known_theories) + "}") |
106 } |
106 } |
107 |
107 |
108 // process |
108 // process |