src/Pure/PIDE/markup_tree.scala
changeset 73120 c3589f2dff31
parent 72815 85aaaf2cd173
child 73359 d8a0e996614b
--- a/src/Pure/PIDE/markup_tree.scala	Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sun Jan 10 13:04:29 2021 +0100
@@ -31,7 +31,7 @@
             case (branches, tree) =>
               (branches /: tree.branches) {
                 case (bs, (r, entry)) =>
-                  require(!bs.isDefinedAt(r))
+                  require(!bs.isDefinedAt(r), "cannot merge markup trees")
                   bs + (r -> entry)
               }
           })