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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
