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 =


isabelle-dev mailing list

Reply via email to