equal
deleted
inserted
replaced
100 ML_Syntax.print_list(ML_Syntax.print_string_bytes))) |
100 ML_Syntax.print_list(ML_Syntax.print_string_bytes))) |
101 |
101 |
102 "Resources.init_session" + |
102 "Resources.init_session" + |
103 "{session_positions = " + print_sessions(sessions_structure.session_positions) + |
103 "{session_positions = " + print_sessions(sessions_structure.session_positions) + |
104 ", session_directories = " + print_table(sessions_structure.dest_session_directories) + |
104 ", session_directories = " + print_table(sessions_structure.dest_session_directories) + |
|
105 ", session_chapters = " + print_table(sessions_structure.session_chapters) + |
105 ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) + |
106 ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) + |
106 ", docs = " + print_list(base.doc_names) + |
107 ", docs = " + print_list(base.doc_names) + |
107 ", global_theories = " + print_table(base.global_theories.toList) + |
108 ", global_theories = " + print_table(base.global_theories.toList) + |
108 ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}" |
109 ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}" |
109 }) |
110 }) |