1.1 --- a/src/Pure/General/position.ML	Mon Aug 15 20:19:41 2011 +0200
     1.2 +++ b/src/Pure/General/position.ML	Mon Aug 15 20:38:16 2011 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val none: T
     1.5    val start: T
     1.6    val file_name: string -> Properties.T
     1.7 +  val file_only: string -> T
     1.8    val file: string -> T
     1.9    val line: int -> T
    1.10    val line_file: int -> string -> T
    1.11 @@ -104,6 +105,7 @@
    1.12  fun file_name "" = []
    1.13    | file_name name = [(Markup.fileN, name)];
    1.14  
    1.15 +fun file_only name = Pos ((0, 0, 0), file_name name);
    1.16  fun file name = Pos ((1, 1, 0), file_name name);
    1.17  
    1.18  fun line_file i name = Pos ((i, 1, 0), file_name name);

     2.1 --- a/src/Pure/General/secure.ML	Mon Aug 15 20:19:41 2011 +0200
     2.2 +++ b/src/Pure/General/secure.ML	Mon Aug 15 20:38:16 2011 +0200
     2.3 @@ -63,7 +63,7 @@
     2.4  val use_file = Secure.use_file;
     2.5  
     2.6  fun use s =
     2.7 -  Position.setmp_thread_data (Position.of_properties (Position.file_name s))
     2.8 +  Position.setmp_thread_data (Position.file_only s)
     2.9      (fn () =>
    2.10        Secure.use_file ML_Parse.global_context true s
    2.11          handle ERROR msg => (writeln msg; error "ML error")) ();

     3.1 --- a/src/Pure/Isar/toplevel.ML	Mon Aug 15 20:19:41 2011 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Aug 15 20:38:16 2011 +0200
     3.3 @@ -185,8 +185,8 @@
     3.4    | _ => raise UNDEF);
     3.5  
     3.6  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
     3.7 -  | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos)
     3.8 -  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos);
     3.9 +  | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos)
    3.10 +  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
    3.11  
    3.12  
    3.13  (* print state *)

     4.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 15 20:19:41 2011 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 20:38:16 2011 +0200
     4.3 @@ -78,7 +78,7 @@
     4.4  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
     4.5  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
     4.6  
     4.7 -fun get_theory (Node {result, ...}) = Toplevel.end_theory Position.none (Lazy.get_finished result);
     4.8 +fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
     4.9  fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
    4.10  
    4.11  val empty_exec = Lazy.value Toplevel.toplevel;
    4.12 @@ -347,7 +347,8 @@
    4.13                      val parents =
    4.14                        imports |> map (fn import =>
    4.15                          (case AList.lookup (op =) deps import of
    4.16 -                          SOME (_, parent_node) => get_theory parent_node
    4.17 +                          SOME (_, parent_node) =>
    4.18 +                            get_theory (Position.file_only (import ^ ".thy")) parent_node
    4.19                          | NONE => Thy_Info.get_theory (Thy_Info.base_name import)));
    4.20                    in Thy_Load.begin_theory dir thy_name imports files parents end
    4.21                  fun get_command id =