# HG changeset patch
# User wenzelm
# Date 1614869355 -3600
# Node ID 4123fca2329675ff7bfea2c2a2ddb84a31f196b8
# Parent  d8a0e996614bb5c43be8c69c907b5f3090aa6f0e
tuned --- fewer warnings;

diff -r d8a0e996614b -r 4123fca23296 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Thu Mar 04 15:41:46 2021 +0100
+++ b/src/Pure/General/graph.scala	Thu Mar 04 15:49:15 2021 +0100
@@ -169,7 +169,7 @@
       else {
         val (rs1, r_set1) =
           if (rev) next(x).foldLeft((rs, r_set + x)) { case (b, a) => reach(a, b) }
-          else (next(x) :\ (rs, r_set + x))(reach)
+          else next(x).foldRight((rs, r_set + x))(reach)
         (x :: rs1, r_set1)
       }
     }
diff -r d8a0e996614b -r 4123fca23296 src/Pure/General/multi_map.scala
--- a/src/Pure/General/multi_map.scala	Thu Mar 04 15:41:46 2021 +0100
+++ b/src/Pure/General/multi_map.scala	Thu Mar 04 15:49:15 2021 +0100
@@ -64,7 +64,7 @@
     else if (isEmpty) other
     else
       other.rep.iterator.foldLeft(this.asInstanceOf[Multi_Map[A, B1]]) {
-        case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
+        case (m1, (a, bs)) => bs.foldRight(m1) { case (b, m2) => m2.insert(a, b) }
       }
 
 
diff -r d8a0e996614b -r 4123fca23296 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Mar 04 15:41:46 2021 +0100
+++ b/src/Pure/General/path.scala	Thu Mar 04 15:49:15 2021 +0100
@@ -54,7 +54,7 @@
     }
 
   private def norm_elems(elems: List[Elem]): List[Elem] =
-    (elems :\ (Nil: List[Elem]))(apply_elem)
+    elems.foldRight(Nil: List[Elem])(apply_elem)
 
   private def implode_elem(elem: Elem, short: Boolean): String =
     elem match {
@@ -174,7 +174,7 @@
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
   def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
 
-  def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
+  def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem))
 
 
   /* implode */
diff -r d8a0e996614b -r 4123fca23296 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Mar 04 15:41:46 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Mar 04 15:49:15 2021 +0100
@@ -733,7 +733,7 @@
 
   def update_properties(more_props: Properties.T): Markup =
     if (more_props.isEmpty) this
-    else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
+    else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) })
 
   def + (entry: Properties.Entry): Markup =
     Markup(name, Properties.put(properties, entry))