155 session_positions: (string * Properties.T) list, |
155 session_positions: (string * Properties.T) list, |
156 session_directories: (string * string) list, |
156 session_directories: (string * string) list, |
157 doc_names: string list, |
157 doc_names: string list, |
158 global_theories: (string * string) list, |
158 global_theories: (string * string) list, |
159 loaded_theories: string list, |
159 loaded_theories: string list, |
160 known_theories: (string * string) list, |
|
161 bibtex_entries: string list}; |
160 bibtex_entries: string list}; |
162 |
161 |
163 fun decode_args yxml = |
162 fun decode_args yxml = |
164 let |
163 let |
165 open XML.Decode; |
164 open XML.Decode; |
166 val position = Position.of_properties o properties; |
165 val position = Position.of_properties o properties; |
167 val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info, |
166 val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info, |
168 (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, |
167 (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, |
169 (theories, (session_positions, (session_directories, (doc_names, (global_theories, |
168 (theories, (session_positions, (session_directories, (doc_names, (global_theories, |
170 (loaded_theories, (known_theories, bibtex_entries)))))))))))))))))) = |
169 (loaded_theories, bibtex_entries))))))))))))))))) = |
171 pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string |
170 pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string |
172 (pair (list (pair string string)) (pair string (pair string (pair string (pair string |
171 (pair (list (pair string string)) (pair string (pair string (pair string (pair string |
173 (pair string |
172 (pair string |
174 (pair (((list (pair Options.decode (list (pair string position)))))) |
173 (pair (((list (pair Options.decode (list (pair string position)))))) |
175 (pair (list (pair string properties)) |
174 (pair (list (pair string properties)) |
176 (pair (list (pair string string)) (pair (list string) |
175 (pair (list (pair string string)) (pair (list string) |
177 (pair (list (pair string string)) (pair (list string) |
176 (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))) |
178 (pair (list (pair string string)) (list string)))))))))))))))))) |
|
179 (YXML.parse_body yxml); |
177 (YXML.parse_body yxml); |
180 in |
178 in |
181 Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, |
179 Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, |
182 verbose = verbose, browser_info = Path.explode browser_info, |
180 verbose = verbose, browser_info = Path.explode browser_info, |
183 document_files = map (apply2 Path.explode) document_files, |
181 document_files = map (apply2 Path.explode) document_files, |
184 graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, |
182 graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, |
185 name = name, master_dir = Path.explode master_dir, theories = theories, |
183 name = name, master_dir = Path.explode master_dir, theories = theories, |
186 session_positions = session_positions, session_directories = session_directories, |
184 session_positions = session_positions, session_directories = session_directories, |
187 doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, |
185 doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, |
188 known_theories = known_theories, bibtex_entries = bibtex_entries} |
186 bibtex_entries = bibtex_entries} |
189 end; |
187 end; |
190 |
188 |
191 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info, |
189 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info, |
192 document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions, |
190 document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions, |
193 session_directories, doc_names, global_theories, loaded_theories, known_theories, |
191 session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = |
194 bibtex_entries}) = |
|
195 let |
192 let |
196 val symbols = HTML.make_symbols symbol_codes; |
193 val symbols = HTML.make_symbols symbol_codes; |
197 |
194 |
198 val _ = |
195 val _ = |
199 Resources.init_session_base |
196 Resources.init_session_base |
200 {session_positions = session_positions, |
197 {session_positions = session_positions, |
201 session_directories = session_directories, |
198 session_directories = session_directories, |
202 docs = doc_names, |
199 docs = doc_names, |
203 global_theories = global_theories, |
200 global_theories = global_theories, |
204 loaded_theories = loaded_theories, |
201 loaded_theories = loaded_theories}; |
205 known_theories = known_theories}; |
|
206 |
202 |
207 val _ = |
203 val _ = |
208 Session.init |
204 Session.init |
209 symbols |
205 symbols |
210 do_output |
206 do_output |