more position information;
authorwenzelm
Wed Apr 19 20:10:34 2017 +0200 (2017-04-19)
changeset 655171544e61e5314
parent 65513 587433a18053
child 65518 bc8fa59211b7
more position information;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     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  
     2.1 --- a/src/Pure/Tools/build.ML	Wed Apr 19 16:26:09 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.ML	Wed Apr 19 20:10:34 2017 +0200
     2.3 @@ -153,13 +153,14 @@
     2.4  fun decode_args yxml =
     2.5    let
     2.6      open XML.Decode;
     2.7 +    val position = Position.of_properties o properties;
     2.8      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
     2.9        (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
    2.10        (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
    2.11        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
    2.12          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    2.13            (pair string
    2.14 -            (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
    2.15 +            (pair (((list (pair Options.decode (list (pair string position))))))
    2.16                (pair (list (pair string string))
    2.17                  (pair (list (pair string string)) (list (pair string string)))))))))))))))
    2.18        (YXML.parse_body yxml);
     3.1 --- a/src/Pure/Tools/build.scala	Wed Apr 19 16:26:09 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 19 20:10:34 2017 +0200
     3.3 @@ -203,7 +203,7 @@
     3.4                pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
     3.5                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     3.6                  pair(string, pair(string, pair(string, pair(Path.encode,
     3.7 -                pair(list(pair(Options.encode, list(string))),
     3.8 +                pair(list(pair(Options.encode, list(pair(string, properties)))),
     3.9                  pair(list(pair(string, string)), pair(list(pair(string, string)),
    3.10                  list(pair(string, string))))))))))))))))(
    3.11                (Symbol.codes, (command_timings, (do_output, (verbose,