src/Pure/PIDE/document.ML
changeset 47051 b32e6de4a39b
parent 46958 0ec8f04e753a
child 47335 693276dcc512
equal deleted inserted replaced
47050:7be54568efa1 47051:b32e6de4a39b
   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