--- 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,