tuned --- fewer warnings;

--- a/src/Tools/jEdit/src/document_model.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -127,7 +127,7 @@
             (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
           }).toList
         if (changed_models.isEmpty) (false, st)
-        else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
+        else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
       })
   }
 
@@ -178,7 +178,9 @@
   {
     GUI_Thread.require {}
     state.change(st =>
-      (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
+      files.foldLeft(st) {
+        case (st1, (node_name, text)) => st1.provide_file(session, node_name, text)
+      })
   }
 
 

--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -121,7 +121,7 @@
       offset: Text.Offset,
       documents: List[Document_Structure.Document]): Unit =
     {
-      (offset /: documents) { case (i, document) =>
+      documents.foldLeft(offset) { case (i, document) =>
         document match {
           case Document_Structure.Block(name, text, body) =>
             val range = Text.Range(i, i + document.length)

--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -257,9 +257,8 @@
         PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match {
           case Some(text) =>
             hyperlink(
-              (Line.Position.zero /:
-                (Symbol.iterator(text).
-                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_)))
+              Symbol.iterator(text).zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1).
+                foldLeft(Line.Position.zero)(_.advance(_)))
           case None =>
             hyperlink(Line.Position((line1 - 1) max 0))
         }

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -363,7 +363,7 @@
           case _ => None
         }).map(_.info)
 
-    gutter_message_content.get((0 /: pris)(_ max _))
+    gutter_message_content.get(pris.foldLeft(0)(_ max _))
   }
 
 
@@ -379,7 +379,7 @@
         {
           case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
         })
-    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
+    val pri = results.foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 
     Rendering.message_background_color.get(pri).map(message_color =>
       {

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -266,8 +266,9 @@
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =
-        if (h <= h_max)
-          (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
+        if (h <= h_max) {
+          split_lines(XML.content(formatted)).foldLeft(0.0)({ case (m, line) => m max metric(line) })
+        }
         else margin
       val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
 

--- a/src/Tools/jEdit/src/text_structure.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -130,7 +130,7 @@
               }).collectFirst({ case (i, true) => i }).getOrElse(0)
 
           def indent_brackets: Int =
-            (0 /: prev_line_span)(
+            prev_line_span.foldLeft(0)(
               { case (i, tok) =>
                   if (tok.is_open_bracket) i + indent_size
                   else if (tok.is_close_bracket) i - indent_size

--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -159,7 +159,7 @@
                 (node_status.failed, PIDE.options.color_value("error_color"))
               ).filter(_._1 > 0)
 
-            ((size.width - 2) /: segments)({ case (last, (n, color)) =>
+            segments.foldLeft(size.width - 2)({ case (last, (n, color)) =>
               val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
               paint_segment(last - w, w, color)
               last - w - 1

--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -182,21 +182,21 @@
 
     val snapshot = PIDE.session.snapshot()
 
-    val iterator =
-      restriction match {
+    val nodes_timing1 =
+      (restriction match {
         case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
         case None => snapshot.version.nodes.iterator
-      }
-    val nodes_timing1 =
-      (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
-          if (PIDE.resources.session_base.loaded_theory(name)) timing1
-          else {
-            val node_timing =
-              Document_Status.Overall_Timing.make(
-                snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
-            timing1 + (name -> node_timing)
-          }
       })
+      .foldLeft(nodes_timing)(
+        { case (timing1, (name, node)) =>
+            if (PIDE.resources.session_base.loaded_theory(name)) timing1
+            else {
+              val node_timing =
+                Document_Status.Overall_Timing.make(
+                  snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
+              timing1 + (name -> node_timing)
+            }
+        })
     nodes_timing = nodes_timing1
 
     val entries = make_entries()