src/Pure/PIDE/document.ML
changeset 54526 92961f196d9e
parent 54519 5fed81762406
child 54558 31844ca390ad
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Nov 20 10:51:47 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Nov 20 11:55:52 2013 +0100
     1.3 @@ -90,9 +90,14 @@
     1.4  
     1.5  fun read_header node span =
     1.6    let
     1.7 -    val (dir, {name = (name, _), imports, keywords}) = get_header node;
     1.8 +    val {name = (name, _), imports, keywords} = #2 (get_header node);
     1.9      val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    1.10 -  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
    1.11 +  in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
    1.12 +
    1.13 +fun master_directory node =
    1.14 +  (case try Url.explode (#1 (get_header node)) of
    1.15 +    SOME (Url.File path) => path
    1.16 +  | _ => Path.current);
    1.17  
    1.18  fun get_perspective (Node {perspective, ...}) = perspective;
    1.19  fun set_perspective args =
    1.20 @@ -329,7 +334,7 @@
    1.21      val blobs' =
    1.22        (commands', Symtab.empty) |->
    1.23          Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
    1.24 -          fold (fn Exn.Res (_, digest) => Symtab.update (digest, the_blob state digest) | _ => I));
    1.25 +          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
    1.26  
    1.27    in (versions', blobs', commands', execution) end);
    1.28  
    1.29 @@ -421,12 +426,8 @@
    1.30  
    1.31  fun init_theory deps node span =
    1.32    let
    1.33 -    (* FIXME provide files via Isabelle/Scala, not master_dir *)
    1.34 -    val (dir, header) = read_header node span;
    1.35 -    val master_dir =
    1.36 -      (case try Url.explode dir of
    1.37 -        SOME (Url.File path) => path
    1.38 -      | _ => Path.current);
    1.39 +    val master_dir = master_directory node;
    1.40 +    val header = read_header node span;
    1.41      val imports = #imports header;
    1.42      val parents =
    1.43        imports |> map (fn (import, _) =>
    1.44 @@ -500,11 +501,12 @@
    1.45        val command_visible = visible_command node command_id';
    1.46        val command_overlays = overlays node command_id';
    1.47        val (command_name, blobs0, span0) = the_command state command_id';
    1.48 -      val blobs = map (Exn.map_result (apsnd (the_blob state))) blobs0;
    1.49 +      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blobs0;
    1.50        val span = Lazy.force span0;
    1.51  
    1.52        val eval' =
    1.53 -        Command.eval (fn () => the_default illegal_init init span) blobs span eval;
    1.54 +        Command.eval (fn () => the_default illegal_init init span)
    1.55 +          (master_directory node) blobs span eval;
    1.56        val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
    1.57        val exec' = (eval', prints');
    1.58