equal
deleted
inserted
replaced
117 last_timing = last_timing}; |
117 last_timing = last_timing}; |
118 val condition = space_explode "," (Options.string options "condition"); |
118 val condition = space_explode "," (Options.string options "condition"); |
119 val conds = filter_out (can getenv_strict) condition; |
119 val conds = filter_out (can getenv_strict) condition; |
120 in |
120 in |
121 if null conds then |
121 if null conds then |
122 (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else (); |
122 (Options.set_default options; |
123 Options.set_default options; |
|
124 Isabelle_Process.init_options (); |
123 Isabelle_Process.init_options (); |
125 Future.fork I; |
124 Future.fork I; |
126 (Thy_Info.use_theories context qualifier master_dir |
125 (Thy_Info.use_theories context qualifier master_dir |
127 |> |
126 |> |
128 (case Options.string options "profiling" of |
127 (case Options.string options "profiling" of |