87 Isabelle_Process.protocol_command "build_session" |
87 Isabelle_Process.protocol_command "build_session" |
88 (fn [args_yxml] => |
88 (fn [args_yxml] => |
89 let |
89 let |
90 val (symbol_codes, (command_timings, (verbose, (browser_info, |
90 val (symbol_codes, (command_timings, (verbose, (browser_info, |
91 (documents, (parent_name, (chapter, (session_name, (master_dir, |
91 (documents, (parent_name, (chapter, (session_name, (master_dir, |
92 (theories, (session_positions, (session_directories, (doc_names, (global_theories, |
92 (theories, (session_positions, (session_directories, (session_chapters, |
93 (loaded_theories, bibtex_entries))))))))))))))) = |
93 (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) = |
94 YXML.parse_body args_yxml |> |
94 YXML.parse_body args_yxml |> |
95 let |
95 let |
96 open XML.Decode; |
96 open XML.Decode; |
97 val position = Position.of_properties o properties; |
97 val position = Position.of_properties o properties; |
98 val path = Path.explode o string; |
98 val path = Path.explode o string; |
100 pair (list (pair string int)) (pair (list properties) (pair bool (pair path |
100 pair (list (pair string int)) (pair (list properties) (pair bool (pair path |
101 (pair (list string) (pair string (pair string (pair string |
101 (pair (list string) (pair string (pair string (pair string |
102 (pair path |
102 (pair path |
103 (pair (((list (pair Options.decode (list (pair string position)))))) |
103 (pair (((list (pair Options.decode (list (pair string position)))))) |
104 (pair (list (pair string properties)) |
104 (pair (list (pair string properties)) |
105 (pair (list (pair string string)) (pair (list string) |
105 (pair (list (pair string string)) |
106 (pair (list (pair string string)) (pair (list string) |
106 (pair (list (pair string string)) (pair (list string) |
107 (list (pair string (list string))))))))))))))))) |
107 (pair (list (pair string string)) (pair (list string) |
|
108 (list (pair string (list string)))))))))))))))))) |
108 end; |
109 end; |
109 |
110 |
110 val symbols = HTML.make_symbols symbol_codes; |
111 val symbols = HTML.make_symbols symbol_codes; |
111 |
112 |
112 fun build () = |
113 fun build () = |
113 let |
114 let |
114 val _ = |
115 val _ = |
115 Resources.init_session |
116 Resources.init_session |
116 {session_positions = session_positions, |
117 {session_positions = session_positions, |
117 session_directories = session_directories, |
118 session_directories = session_directories, |
|
119 session_chapters = session_chapters, |
118 bibtex_entries = bibtex_entries, |
120 bibtex_entries = bibtex_entries, |
119 docs = doc_names, |
121 docs = doc_names, |
120 global_theories = global_theories, |
122 global_theories = global_theories, |
121 loaded_theories = loaded_theories}; |
123 loaded_theories = loaded_theories}; |
122 |
124 |