more informative error message;
authorwenzelm
Mon Jan 06 19:59:43 2014 +0100 (2014-01-06)
changeset 54939b411e99d1581
parent 54938 8cccfb8f1d36
child 54940 a20b105bb5d1
more informative error message;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Mon Jan 06 19:47:11 2014 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Jan 06 19:59:43 2014 +0100
     1.3 @@ -117,7 +117,8 @@
     1.4          (Graph.string[Session_Info] /: infos) {
     1.5            case (graph, (name, info)) =>
     1.6              if (graph.defined(name))
     1.7 -              error("Duplicate session " + quote(name) + Position.here(info.pos))
     1.8 +              error("Duplicate session " + quote(name) + Position.here(info.pos) +
     1.9 +                Position.here(graph.get_node(name).pos))
    1.10              else graph.new_node(name, info)
    1.11          }
    1.12        val graph2 =