equal
deleted
inserted
replaced
443 is_some (Exn.get_res (get_header (get_node nodes name))); |
443 is_some (Exn.get_res (get_header (get_node nodes name))); |
444 |
444 |
445 fun init_theory deps node = |
445 fun init_theory deps node = |
446 let |
446 let |
447 (* FIXME provide files via Scala layer, not master_dir *) |
447 (* FIXME provide files via Scala layer, not master_dir *) |
448 val (master_dir, header) = Exn.release (get_header node); |
448 val (dir, header) = Exn.release (get_header node); |
|
449 val master_dir = |
|
450 (case Url.explode dir of |
|
451 Url.File path => path |
|
452 | _ => Path.current); |
449 val parents = |
453 val parents = |
450 #imports header |> map (fn import => |
454 #imports header |> map (fn import => |
451 (case Thy_Info.lookup_theory import of (* FIXME more robust!? *) |
455 (case Thy_Info.lookup_theory import of (* FIXME more robust!? *) |
452 SOME thy => thy |
456 SOME thy => thy |
453 | NONE => |
457 | NONE => |
454 get_theory (Position.file_only import) |
458 get_theory (Position.file_only import) |
455 (snd (Future.join (the (AList.lookup (op =) deps import)))))); |
459 (snd (Future.join (the (AList.lookup (op =) deps import)))))); |
456 in Thy_Load.begin_theory (Path.explode master_dir) header parents end; |
460 in Thy_Load.begin_theory master_dir header parents end; |
457 |
461 |
458 in |
462 in |
459 |
463 |
460 fun update (old_id: version_id) (new_id: version_id) edits state = |
464 fun update (old_id: version_id) (new_id: version_id) edits state = |
461 let |
465 let |