src/Pure/Thy/thy_load.ML

 *)
 
 signature THY_LOAD =
 sig
   val master_directory: theory -> Path.T
-  val imports_of: theory -> string list
+  val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
   val parse_files: string -> (theory -> Token.file list) parser
   val check_thy: Path.T -> string ->
-   {master: Path.T * SHA1.digest, text: string, imports: string list,
+   {master: Path.T * SHA1.digest, text: string, imports: (string * Position.T) list,
     uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
   val provide: Path.T * SHA1.digest -> theory -> theory
   val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
   val use_file: Path.T -> theory -> string * theory

 
 (* manage source files *)
 
 type files =
  {master_dir: Path.T,  (*master directory of theory source*)
-  imports: string list,  (*source specification of imports*)
+  imports: (string * Position.T) list,  (*source specification of imports*)
   provided: (Path.T * SHA1.digest) list};  (*source path, digest*)
 
 fun make_files (master_dir, imports, provided): files =
  {master_dir = master_dir, imports = imports, provided = provided};
 

   let
     val path = thy_path (Path.basic thy_name);
     val master_file = check_file dir path;
     val text = File.read master_file;
 
-    val {name, imports, uses, keywords} = Thy_Header.read (Path.position master_file) text;
+    val {name = (name, pos), imports, uses, keywords} =
+      Thy_Header.read (Path.position master_file) text;
     val _ = thy_name <> name andalso
-      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name);
+      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.str_of pos);
   in
    {master = (master_file, SHA1.digest text), text = text,
     imports = imports, uses = uses, keywords = keywords}
   end;
 

       fold_map element_result elements (Toplevel.toplevel, Position.none);
 
     val thy = Toplevel.end_theory end_pos end_state;
   in (flat results, thy) end;
 
-fun load_thy update_time master_dir header pos text parents =
+fun load_thy update_time master_dir header text_pos text parents =
   let
     val time = ! Toplevel.timing;
 
-    val {name, uses, ...} = header;
+    val {name = (name, _), uses, ...} = header;
     val _ = Thy_Header.define_keywords header;
     val _ = Present.init_theory name;
     fun init () =
       begin_theory master_dir header parents
       |> Present.begin_theory update_time master_dir uses;
 
     val lexs = Keyword.get_lexicons ();
 
-    val toks = Thy_Syntax.parse_tokens lexs pos text;
+    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
     val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks);
     val elements = Thy_Syntax.parse_elements spans;
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);