[isabelle-dev] Can I request an improvement to the error for "Duplicate session"

[Thomas Sewell]

Hey Isabelle devs.

I've just spent a few minutes helping a teammate who was getting 
"Duplicate session" errors out of isabelle build/jedit.

To reproduce this error, take a version of isabelle at, say, 
~tsewell/work/isabelle, and attempt "isabelle jedit -d . -d 
~tsewell/work/isabelle".

(Needless to say, the additional -d parameter was passed implicitly in 
my colleague's setup, or else we would have figured this out much faster.)

Anyway, this would all be a lot easier to understand if 
isabelle/src/Pure/Tools/build.scala reported both the duplicate 
specification addresses.

At enormous risk of offending the wizards of the realm by appallingly 
wasting their time, this is a patch that solves the issue:

diff -r 22d0c7fe0dfa -r 0d2b3391c1d9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala    Fri Dec 20 17:15:40 2013 +1100
+++ b/src/Pure/Tools/build.scala    Mon Dec 23 13:26:55 2013 +1100
@@ -117,7 +117,9 @@
          (Graph.string[Session_Info] /: infos) {
            case (graph, (name, info)) =>
              if (graph.defined(name))
-              error("Duplicate session " + quote(name) + 
Position.here(info.pos))
+              error("Duplicate session " + quote(name)
+                + Position.here(info.pos)
+                + Position.here(graph.get_node(name).pos))
              else graph.new_node(name, info)
          }
        val graph2 =


Cheers,
     Thomas.