# HG changeset patch
# User wenzelm
# Date 1346011827 -7200
# Node ID 698fb0e27b111f8d7aa2fa89a4b276b5085e40f6
# Parent  ef462b5558ebed5b2991e0c020712a7c8349c122
more accurate defining position of theory;

diff -r ef462b5558eb -r 698fb0e27b11 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Aug 26 21:46:50 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Aug 26 22:10:27 2012 +0200
@@ -239,27 +239,27 @@
 
 fun check_deps dir name =
   (case lookup_deps name of
-    SOME NONE => (true, NONE, get_imports name, [], [])
+    SOME NONE => (true, NONE, Position.none, get_imports name, [], [])
   | NONE =>
-      let val {master, text, imports, keywords, uses} = Thy_Load.check_thy dir name
-      in (false, SOME (make_deps master imports, text), imports, uses, keywords) end
+      let val {master, text, theory_pos, imports, keywords, uses} = Thy_Load.check_thy dir name
+      in (false, SOME (make_deps master imports, text), theory_pos, imports, uses, keywords) end
   | SOME (SOME {master, ...}) =>
       let
-        val {master = master', text = text', imports = imports', uses = uses', keywords = keywords'}
-          = Thy_Load.check_thy dir name;
+        val {master = master', text = text', theory_pos = theory_pos', imports = imports',
+          uses = uses', keywords = keywords'} = Thy_Load.check_thy dir name;
         val deps' = SOME (make_deps master' imports', text');
         val current =
           #2 master = #2 master' andalso
             (case lookup_theory name of
               NONE => false
             | SOME theory => Thy_Load.load_current theory);
-      in (current, deps', imports', uses', keywords') end);
+      in (current, deps', theory_pos', imports', uses', keywords') end);
 
 in
 
 fun require_thys initiators dir strs tasks =
       fold_map (require_thy initiators dir) strs tasks |>> forall I
-and require_thy initiators dir (str, pos) tasks =
+and require_thy initiators dir (str, require_pos) tasks =
   let
     val path = Path.expand (Path.explode str);
     val name = Path.implode (Path.base path);
@@ -271,10 +271,10 @@
           val dir' = Path.append dir (Path.dir path);
           val _ = member (op =) initiators name andalso error (cycle_msg initiators);
 
-          val (current, deps, imports, uses, keywords) = check_deps dir' name
+          val (current, deps, theory_pos, imports, uses, keywords) = check_deps dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
-                Position.str_of pos ^ required_by "\n" initiators);
+                Position.str_of require_pos ^ required_by "\n" initiators);
 
           val parents = map (base_name o #1) imports;
           val (parents_current, tasks') =
@@ -290,7 +290,8 @@
               | SOME (dep, text) =>
                   let
                     val update_time = serial ();
-                    val load = load_thy initiators update_time dep text (name, pos) uses keywords;
+                    val load =
+                      load_thy initiators update_time dep text (name, theory_pos) uses keywords;
                   in Task (parents, load) end);
 
           val tasks'' = new_entry name parents task tasks';
diff -r ef462b5558eb -r 698fb0e27b11 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sun Aug 26 21:46:50 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sun Aug 26 22:10:27 2012 +0200
@@ -11,8 +11,8 @@
   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 * Position.T) list,
-    uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
+   {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
+    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
@@ -137,7 +137,7 @@
     val _ = thy_name <> name andalso
       error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.str_of pos);
   in
-   {master = (master_file, SHA1.digest text), text = text,
+   {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, uses = uses, keywords = keywords}
   end;