more checks;
authorwenzelm
Fri Apr 07 13:27:47 2017 +0200 (2017-04-07 ago)
changeset 65424741d40f42dd3
parent 65423 4527b33d5b3e
child 65425 b168a648988e
more checks;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 07 13:19:11 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 13:27:47 2017 +0200
     1.3 @@ -290,10 +290,16 @@
     1.4        if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
     1.5  
     1.6      def global_theories: Set[String] =
     1.7 -      (for {
     1.8 -        (_, (info, _)) <- imports_graph.iterator
     1.9 -        name <- info.global_theories.iterator }
    1.10 -       yield name).toSet
    1.11 +      (Set.empty[String] /:
    1.12 +        (for {
    1.13 +          (_, (info, _)) <- imports_graph.iterator
    1.14 +          thy <- info.global_theories.iterator }
    1.15 +         yield (thy, info.pos)))(
    1.16 +          { case (set, (thy, pos)) =>
    1.17 +             if (set.contains(thy))
    1.18 +               error("Duplicate declaration of global theory " + quote(thy) + Position.here(pos))
    1.19 +             else set + thy
    1.20 +           })
    1.21  
    1.22      def selection(select: Selection): (List[String], T) =
    1.23      {