eliminate odd workaround from Aug-2012 (see 393a37003851);
authorwenzelm
Sat, 28 Jun 2025 12:27:43 +0200
changeset 82788 5afb8d0d418e
parent 82787 ddb68e3058d3
child 82789 941b6cdf3611
eliminate odd workaround from Aug-2012 (see 393a37003851);
src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Jun 28 12:22:03 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jun 28 12:27:43 2025 +0200
@@ -328,9 +328,7 @@
         var nodes = nodes0
         val doc_edits = mutable.ListBuffer.from(doc_edits0)
 
-        val node_edits =
-          (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
-            .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
+        val node_edits = (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
 
         node_edits foreach {
           case (name, edits) =>