# HG changeset patch
# User wenzelm
# Date 1661543353 -7200
# Node ID aaa0148e7c8ff37538a7f162d51a2acd4e36b289
# Parent  46c6f649a943223f2fb4c0c64159296d2a00381d
clarified signature;

diff -r 46c6f649a943 -r aaa0148e7c8f src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Fri Aug 26 21:48:51 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Fri Aug 26 21:49:13 2022 +0200
@@ -135,8 +135,12 @@
     }
 
     sealed case class Index(kind: String, items: List[Item]) {
-      def +(item: Item): Index =
-        Index(kind, (item :: items.filterNot(_.name == item.name)).sortBy(_.name))
+      def ++ (more_items: List[Item]): Index = {
+        val items1 = items.filterNot(item => more_items.exists(_.name == item.name))
+        val items2 = (more_items ::: items1).sortBy(_.name)
+        Index(kind, items2)
+      }
+      def + (item: Item): Index = this ++ List(item)
 
       def json: JSON.T = JSON.Object("kind" -> kind, "items" -> items.map(_.json))
       def print_json: JSON.S = JSON.Format.pretty_print(json)
@@ -323,7 +327,7 @@
               (name, _) <- sessions_structure.chapters.iterator
               if !items1.exists(_.name == name)
             } yield Meta_Data.Item(name)).toList
-          (items1 ::: items2).foldLeft(index0)(_ + _)
+          index0 ++ (items1 ::: items2)
         }
         val chapters = index.items