src/Pure/Thy/sessions.scala
changeset 65517 1544e61e5314
parent 65507 decdb95bd007
child 65519 d244d8f8e13f
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Apr 19 16:26:09 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Apr 19 20:10:34 2017 +0200
     1.3 @@ -164,8 +164,8 @@
     1.4              {
     1.5                val root_theories =
     1.6                  info.theories.flatMap({ case (_, thys) =>
     1.7 -                  thys.map(thy =>
     1.8 -                    (resources.import_name(session_name, info.dir.implode, thy), info.pos))
     1.9 +                  thys.map({ case (thy, pos) =>
    1.10 +                    (resources.import_name(session_name, info.dir.implode, thy), pos) })
    1.11                  })
    1.12                val thy_deps = resources.thy_info.dependencies(root_theories)
    1.13  
    1.14 @@ -292,7 +292,7 @@
    1.15      description: String,
    1.16      options: Options,
    1.17      imports: List[String],
    1.18 -    theories: List[(Options, List[String])],
    1.19 +    theories: List[(Options, List[(String, Position.T)])],
    1.20      global_theories: List[String],
    1.21      files: List[Path],
    1.22      document_files: List[(Path, Path)],
    1.23 @@ -491,7 +491,7 @@
    1.24        description: String,
    1.25        options: List[Options.Spec],
    1.26        imports: List[String],
    1.27 -      theories: List[(List[Options.Spec], List[(String, Boolean)])],
    1.28 +      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    1.29        files: List[String],
    1.30        document_files: List[(String, String)]) extends Entry
    1.31  
    1.32 @@ -515,7 +515,7 @@
    1.33          ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
    1.34  
    1.35        val theory_entry =
    1.36 -        theory_name ~ global ^^ { case x ~ y => (x, y) }
    1.37 +        position(theory_name) ~ global ^^ { case x ~ y => (x, y) }
    1.38  
    1.39        val theories =
    1.40          $$$(THEORIES) ~!
    1.41 @@ -561,11 +561,12 @@
    1.42              entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
    1.43  
    1.44            val global_theories =
    1.45 -            for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
    1.46 +            for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
    1.47              yield {
    1.48                val thy_name = Path.explode(thy).expand.base.implode
    1.49                if (Long_Name.is_qualified(thy_name))
    1.50 -                error("Bad qualified name for global theory " + quote(thy_name))
    1.51 +                error("Bad qualified name for global theory " +
    1.52 +                  quote(thy_name) + Position.here(pos))
    1.53                else thy_name
    1.54              }
    1.55