equal
deleted
inserted
replaced
258 raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); |
258 raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); |
259 |
259 |
260 val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); |
260 val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); |
261 val (theory, present, weight) = |
261 val (theory, present, weight) = |
262 Resources.load_thy document symbols last_timing update_time dir header text_pos text |
262 Resources.load_thy document symbols last_timing update_time dir header text_pos text |
263 (if name = Context.PureN then [ML_Context.the_global_context ()] else parents); |
263 (if name = Context.PureN then [Context.the_global_context ()] else parents); |
264 fun commit () = update_thy deps theory; |
264 fun commit () = update_thy deps theory; |
265 in |
265 in |
266 Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} |
266 Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} |
267 end; |
267 end; |
268 |
268 |