53 in y end; |
53 in y end; |
54 |
54 |
55 |
55 |
56 (* build theories *) |
56 (* build theories *) |
57 |
57 |
58 fun build_theories symbols last_timing qualifier master_dir (options, thys) = |
58 fun build_theories last_timing qualifier master_dir (options, thys) = |
59 let |
59 let |
60 val context = |
60 val context = {options = options, last_timing = last_timing}; |
61 {options = options, symbols = symbols, last_timing = last_timing}; |
|
62 val condition = space_explode "," (Options.string options "condition"); |
61 val condition = space_explode "," (Options.string options "condition"); |
63 val conds = filter_out (can getenv_strict) condition; |
62 val conds = filter_out (can getenv_strict) condition; |
64 in |
63 in |
65 if null conds then |
64 if null conds then |
66 (Options.set_default options; |
65 (Options.set_default options; |
85 |
84 |
86 val _ = |
85 val _ = |
87 Isabelle_Process.protocol_command "build_session" |
86 Isabelle_Process.protocol_command "build_session" |
88 (fn [args_yxml] => |
87 (fn [args_yxml] => |
89 let |
88 let |
90 val (symbol_codes, (command_timings, (verbose, (browser_info, |
89 val (html_symbols, (command_timings, (verbose, (browser_info, |
91 (documents, (parent_name, (chapter, (session_name, (master_dir, |
90 (documents, (parent_name, (chapter, (session_name, (master_dir, |
92 (theories, (session_positions, (session_directories, (session_chapters, |
91 (theories, (session_positions, (session_directories, (session_chapters, |
93 (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) = |
92 (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) = |
94 YXML.parse_body args_yxml |> |
93 YXML.parse_body args_yxml |> |
95 let |
94 let |
106 (pair (list (pair string string)) (pair (list string) |
105 (pair (list (pair string string)) (pair (list string) |
107 (pair (list (pair string string)) (pair (list string) |
106 (pair (list (pair string string)) (pair (list string) |
108 (list (pair string (list string)))))))))))))))))) |
107 (list (pair string (list string)))))))))))))))))) |
109 end; |
108 end; |
110 |
109 |
111 val symbols = HTML.make_symbols symbol_codes; |
|
112 |
|
113 fun build () = |
110 fun build () = |
114 let |
111 let |
115 val _ = |
112 val _ = |
116 Resources.init_session |
113 Resources.init_session |
117 {session_positions = session_positions, |
114 {html_symbols = html_symbols, |
|
115 session_positions = session_positions, |
118 session_directories = session_directories, |
116 session_directories = session_directories, |
119 session_chapters = session_chapters, |
117 session_chapters = session_chapters, |
120 bibtex_entries = bibtex_entries, |
118 bibtex_entries = bibtex_entries, |
121 docs = doc_names, |
119 docs = doc_names, |
122 global_theories = global_theories, |
120 global_theories = global_theories, |
123 loaded_theories = loaded_theories}; |
121 loaded_theories = loaded_theories}; |
124 |
122 |
125 val _ = |
123 val _ = |
126 Session.init |
124 Session.init |
127 symbols |
|
128 (Options.default_bool "browser_info") |
125 (Options.default_bool "browser_info") |
129 browser_info |
126 browser_info |
130 documents |
127 documents |
131 parent_name |
128 parent_name |
132 (chapter, session_name) |
129 (chapter, session_name) |