more position information;

--- a/src/Pure/Thy/sessions.scala	Wed Apr 19 16:26:09 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 19 20:10:34 2017 +0200
@@ -164,8 +164,8 @@
             {
               val root_theories =
                 info.theories.flatMap({ case (_, thys) =>
-                  thys.map(thy =>
-                    (resources.import_name(session_name, info.dir.implode, thy), info.pos))
+                  thys.map({ case (thy, pos) =>
+                    (resources.import_name(session_name, info.dir.implode, thy), pos) })
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
@@ -292,7 +292,7 @@
     description: String,
     options: Options,
     imports: List[String],
-    theories: List[(Options, List[String])],
+    theories: List[(Options, List[(String, Position.T)])],
     global_theories: List[String],
     files: List[Path],
     document_files: List[(Path, Path)],
@@ -491,7 +491,7 @@
       description: String,
       options: List[Options.Spec],
       imports: List[String],
-      theories: List[(List[Options.Spec], List[(String, Boolean)])],
+      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
       files: List[String],
       document_files: List[(String, String)]) extends Entry
 
@@ -515,7 +515,7 @@
         ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
 
       val theory_entry =
-        theory_name ~ global ^^ { case x ~ y => (x, y) }
+        position(theory_name) ~ global ^^ { case x ~ y => (x, y) }
 
       val theories =
         $$$(THEORIES) ~!
@@ -561,11 +561,12 @@
             entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
 
           val global_theories =
-            for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
+            for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
             yield {
               val thy_name = Path.explode(thy).expand.base.implode
               if (Long_Name.is_qualified(thy_name))
-                error("Bad qualified name for global theory " + quote(thy_name))
+                error("Bad qualified name for global theory " +
+                  quote(thy_name) + Position.here(pos))
               else thy_name
             }
 

--- a/src/Pure/Tools/build.ML	Wed Apr 19 16:26:09 2017 +0200
+++ b/src/Pure/Tools/build.ML	Wed Apr 19 20:10:34 2017 +0200
@@ -153,13 +153,14 @@
 fun decode_args yxml =
   let
     open XML.Decode;
+    val position = Position.of_properties o properties;
     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
       (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
           (pair string
-            (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
+            (pair (((list (pair Options.decode (list (pair string position))))))
               (pair (list (pair string string))
                 (pair (list (pair string string)) (list (pair string string)))))))))))))))
       (YXML.parse_body yxml);

--- a/src/Pure/Tools/build.scala	Wed Apr 19 16:26:09 2017 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 19 20:10:34 2017 +0200
@@ -203,7 +203,7 @@
               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
-                pair(list(pair(Options.encode, list(string))),
+                pair(list(pair(Options.encode, list(pair(string, properties)))),
                 pair(list(pair(string, string)), pair(list(pair(string, string)),
                 list(pair(string, string))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,