1.1 --- a/src/Pure/PIDE/document.ML	Wed Mar 14 22:34:18 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 15 00:10:45 2012 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    val new_id: unit -> id
     1.5    val parse_id: string -> id
     1.6    val print_id: id -> string
     1.7 -  type node_header = ((string * string) * string list * (string * bool) list) Exn.result
     1.8 +  type node_header = (string * Thy_Header.header) Exn.result
     1.9    datatype node_edit =
    1.10      Clear |
    1.11      Edits of (command_id option * command_id option) list |
    1.12 @@ -58,7 +58,7 @@
    1.13  
    1.14  (** document structure **)
    1.15  
    1.16 -type node_header = ((string * string) * string list * (string * bool) list) Exn.result;
    1.17 +type node_header = (string * Thy_Header.header) Exn.result;
    1.18  type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
    1.19  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.20  
    1.21 @@ -212,7 +212,7 @@
    1.22          |> touch_node name
    1.23      | Header header =>
    1.24          let
    1.25 -          val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
    1.26 +          val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
    1.27            val nodes1 = nodes
    1.28              |> default_node name
    1.29              |> fold default_node imports;
    1.30 @@ -307,7 +307,6 @@
    1.31  end;
    1.32  
    1.33  
    1.34 -
    1.35  (* toplevel transactions *)
    1.36  
    1.37  local
    1.38 @@ -447,16 +446,15 @@
    1.39  fun init_theory deps node =
    1.40    let
    1.41      (* FIXME provide files via Scala layer, not master_dir *)
    1.42 -    val ((master_dir, thy_name), imports, uses) = Exn.release (get_header node);
    1.43 -    val files = map (apfst Path.explode) uses;
    1.44 +    val (master_dir, header) = Exn.release (get_header node);
    1.45      val parents =
    1.46 -      imports |> map (fn import =>
    1.47 +      #imports header |> map (fn import =>
    1.48          (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
    1.49            SOME thy => thy
    1.50          | NONE =>
    1.51              get_theory (Position.file_only import)
    1.52                (snd (Future.join (the (AList.lookup (op =) deps import))))));
    1.53 -  in Thy_Load.begin_theory (Path.explode master_dir) thy_name imports files parents end;
    1.54 +  in Thy_Load.begin_theory (Path.explode master_dir) header parents end;
    1.55  
    1.56  in
    1.57