# HG changeset patch # User wenzelm # Date 1614808126 -3600 # Node ID 78aa7846e91fe11fd90c7990112922d9e44d3ffb # Parent 31d4274f32de27975fd5a038df14418a75123f8b tuned --- fewer warnings; diff -r 31d4274f32de -r 78aa7846e91f src/Tools/jEdit/src/document_model.scala --- 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) + }) } diff -r 31d4274f32de -r 78aa7846e91f src/Tools/jEdit/src/isabelle_sidekick.scala --- 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) diff -r 31d4274f32de -r 78aa7846e91f src/Tools/jEdit/src/jedit_editor.scala --- 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)) } diff -r 31d4274f32de -r 78aa7846e91f src/Tools/jEdit/src/jedit_rendering.scala --- 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 => { diff -r 31d4274f32de -r 78aa7846e91f src/Tools/jEdit/src/pretty_tooltip.scala --- 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 diff -r 31d4274f32de -r 78aa7846e91f src/Tools/jEdit/src/text_structure.scala --- 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 diff -r 31d4274f32de -r 78aa7846e91f src/Tools/jEdit/src/theories_dockable.scala --- 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 diff -r 31d4274f32de -r 78aa7846e91f src/Tools/jEdit/src/timing_dockable.scala --- 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()