83 Isabelle_System.chmod("600", File.path(init_session)) |
83 Isabelle_System.chmod("600", File.path(init_session)) |
84 File.write(init_session, |
84 File.write(init_session, |
85 session_base match { |
85 session_base match { |
86 case None => "" |
86 case None => "" |
87 case Some(base) => |
87 case Some(base) => |
|
88 def print_symbols: List[(String, Int)] => String = |
|
89 ML_Syntax.print_list( |
|
90 ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_int)) |
88 def print_table: List[(String, String)] => String = |
91 def print_table: List[(String, String)] => String = |
89 ML_Syntax.print_list( |
92 ML_Syntax.print_list( |
90 ML_Syntax.print_pair( |
93 ML_Syntax.print_pair( |
91 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes)) |
94 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes)) |
92 def print_list: List[String] => String = |
95 def print_list: List[String] => String = |
98 ML_Syntax.print_list( |
101 ML_Syntax.print_list( |
99 ML_Syntax.print_pair(ML_Syntax.print_string_bytes, |
102 ML_Syntax.print_pair(ML_Syntax.print_string_bytes, |
100 ML_Syntax.print_list(ML_Syntax.print_string_bytes))) |
103 ML_Syntax.print_list(ML_Syntax.print_string_bytes))) |
101 |
104 |
102 "Resources.init_session" + |
105 "Resources.init_session" + |
103 "{session_positions = " + print_sessions(sessions_structure.session_positions) + |
106 "{html_symbols = " + print_symbols(Symbol.codes) + |
|
107 ", session_positions = " + print_sessions(sessions_structure.session_positions) + |
104 ", session_directories = " + print_table(sessions_structure.dest_session_directories) + |
108 ", session_directories = " + print_table(sessions_structure.dest_session_directories) + |
105 ", session_chapters = " + print_table(sessions_structure.session_chapters) + |
109 ", session_chapters = " + print_table(sessions_structure.session_chapters) + |
106 ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) + |
110 ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) + |
107 ", docs = " + print_list(base.doc_names) + |
111 ", docs = " + print_list(base.doc_names) + |
108 ", global_theories = " + print_table(base.global_theories.toList) + |
112 ", global_theories = " + print_table(base.global_theories.toList) + |