src/Pure/PIDE/document.ML
changeset 44200 ce0112e26b3b
parent 44199 e38885e3ea60
child 44201 6429ab1b6883
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 15 20:19:41 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 20:38:16 2011 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
     1.5  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
     1.6  
     1.7 -fun get_theory (Node {result, ...}) = Toplevel.end_theory Position.none (Lazy.get_finished result);
     1.8 +fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
     1.9  fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
    1.10  
    1.11  val empty_exec = Lazy.value Toplevel.toplevel;
    1.12 @@ -347,7 +347,8 @@
    1.13                      val parents =
    1.14                        imports |> map (fn import =>
    1.15                          (case AList.lookup (op =) deps import of
    1.16 -                          SOME (_, parent_node) => get_theory parent_node
    1.17 +                          SOME (_, parent_node) =>
    1.18 +                            get_theory (Position.file_only (import ^ ".thy")) parent_node
    1.19                          | NONE => Thy_Info.get_theory (Thy_Info.base_name import)));
    1.20                    in Thy_Load.begin_theory dir thy_name imports files parents end
    1.21                  fun get_command id =