tuned;

--- a/src/Pure/GUI/gui.scala	Tue Dec 27 11:44:37 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Tue Dec 27 12:00:37 2022 +0100
@@ -153,9 +153,7 @@
     }
 
     private def make_entries[A](batches: List[List[Entry[A]]]): List[Entry[A]] = {
-      val item_batches =
-        batches.map(_.flatMap(
-          { case item: Item[_] => Some(item.asInstanceOf[Item[A]]) case _ => None }))
+      val item_batches = batches.map(_.flatMap(Library.as_subclass(classOf[Item[A]])))
       val sep_entries: List[Entry[A]] =
         item_batches.filter(_.nonEmpty).zipWithIndex.flatMap({ case (batch, i) =>
           Separator[A](i) :: batch.map(_.copy(batch = i))

--- a/src/Pure/Thy/sessions.scala	Tue Dec 27 11:44:37 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Dec 27 12:00:37 2022 +0100
@@ -1100,8 +1100,7 @@
   def parse_root(path: Path): List[Entry] = Parsers.parse_root(path)
 
   def parse_root_entries(path: Path): List[Session_Entry] =
-    for (entry <- Parsers.parse_root(path) if entry.isInstanceOf[Session_Entry])
-    yield entry.asInstanceOf[Session_Entry]
+    Parsers.parse_root(path).flatMap(Library.as_subclass(classOf[Session_Entry]))
 
   def parse_roots(roots: Path): List[String] = {
     for {

--- a/src/Tools/jEdit/src/document_model.scala	Tue Dec 27 11:44:37 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 27 12:00:37 2022 +0100
@@ -32,8 +32,8 @@
     def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
       for {
         (node_name, model) <- models.iterator
-        if model.isInstanceOf[File_Model]
-      } yield (node_name, model.asInstanceOf[File_Model])
+        file_model <- Library.as_subclass(classOf[File_Model])(model)
+      } yield (node_name, file_model)
 
     def document_blobs: Document.Blobs =
       Document.Blobs(