# HG changeset patch
# User wenzelm
# Date 1614869528 -3600
# Node ID ef8c9b3d53558afeaf36181303b646b7ef84606d
# Parent  4123fca2329675ff7bfea2c2a2ddb84a31f196b8
tuned;

diff -r 4123fca23296 -r ef8c9b3d5355 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Mar 04 15:49:15 2021 +0100
+++ b/src/Pure/General/path.scala	Thu Mar 04 15:52:08 2021 +0100
@@ -54,7 +54,7 @@
     }
 
   private def norm_elems(elems: List[Elem]): List[Elem] =
-    elems.foldRight(Nil: List[Elem])(apply_elem)
+    elems.foldRight(List.empty[Elem])(apply_elem)
 
   private def implode_elem(elem: Elem, short: Boolean): String =
     elem match {
diff -r 4123fca23296 -r ef8c9b3d5355 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Mar 04 15:49:15 2021 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 04 15:52:08 2021 +0100
@@ -1027,7 +1027,7 @@
         if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
 
       val (changed_commands, new_execs) =
-        update.foldLeft((Nil: List[Command], execs)) {
+        update.foldLeft((List.empty[Command], execs)) {
           case ((commands1, execs1), (command_id, exec)) =>
             val st = the_static_state(command_id)
             val command = st.command
diff -r 4123fca23296 -r ef8c9b3d5355 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 04 15:49:15 2021 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 04 15:52:08 2021 +0100
@@ -94,7 +94,7 @@
 
         case (elems, body) =>
           val (end_offset, subtrees) =
-             body.foldLeft((offset, Nil: List[Markup_Tree]))(make_trees)
+             body.foldLeft((offset, List.empty[Markup_Tree]))(make_trees)
           if (offset == end_offset) acc
           else {
             val range = Text.Range(offset, end_offset)
@@ -105,7 +105,7 @@
     }
 
   def from_XML(body: XML.Body): Markup_Tree =
-    merge_disjoint(body.foldLeft((0, Nil: List[Markup_Tree]))(make_trees)._2)
+    merge_disjoint(body.foldLeft((0, List.empty[Markup_Tree]))(make_trees)._2)
 }
 
 
diff -r 4123fca23296 -r ef8c9b3d5355 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Thu Mar 04 15:49:15 2021 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Thu Mar 04 15:52:08 2021 +0100
@@ -25,7 +25,7 @@
 {
   /* status */
 
-  private val status = new ListView(Nil: List[Document.Node.Name]) {
+  private val status = new ListView(List.empty[Document.Node.Name]) {
     background =
     {
       // enforce default value
diff -r 4123fca23296 -r ef8c9b3d5355 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Thu Mar 04 15:49:15 2021 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Mar 04 15:52:08 2021 +0100
@@ -104,7 +104,7 @@
 
   /* timing view */
 
-  private val timing_view = new ListView(Nil: List[Entry]) {
+  private val timing_view = new ListView(List.empty[Entry]) {
     listenTo(mouse.clicks)
     reactions += {
       case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>