# HG changeset patch # User wenzelm # Date 1614868906 -3600 # Node ID d8a0e996614bb5c43be8c69c907b5f3090aa6f0e # Parent 78aa7846e91fe11fd90c7990112922d9e44d3ffb tuned --- fewer warnings; diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Admin/afp.scala --- a/src/Pure/Admin/afp.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Admin/afp.scala Thu Mar 04 15:41:46 2021 +0100 @@ -136,7 +136,7 @@ } val entries_map = - (SortedMap.empty[String, AFP.Entry] /: entries)({ case (m, e) => m + (e.name -> e) }) + entries.foldLeft(SortedMap.empty[String, AFP.Entry]) { case (m, e) => m + (e.name -> e) } val extra_metadata = (for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name). @@ -153,8 +153,9 @@ /* sessions */ val sessions_map: SortedMap[String, AFP.Entry] = - (SortedMap.empty[String, AFP.Entry] /: entries)( - { case (m1, e) => (m1 /: e.sessions)({ case (m2, s) => m2 + (s -> e) }) }) + entries.foldLeft(SortedMap.empty[String, AFP.Entry]) { + case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e) } + } val sessions: List[String] = entries.flatMap(_.sessions) @@ -171,22 +172,25 @@ lazy val entries_graph: Graph[String, Unit] = { val session_entries = - (Map.empty[String, String] /: entries) { - case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) } + entries.foldLeft(Map.empty[String, String]) { + case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e.name) } } - (Graph.empty[String, Unit] /: entries) { case (g, entry) => - val e1 = entry.name - (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) => - (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) => - try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) } - catch { - case exn: Graph.Cycles[_] => - error(cat_lines(exn.cycles.map(cycle => - "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") + - " due to session " + quote(s)))) - } + entries.foldLeft(Graph.empty[String, Unit]) { + case (g, entry) => + val e1 = entry.name + sessions_deps(entry).foldLeft(g.default_node(e1, ())) { + case (g1, s) => + session_entries.get(s).filterNot(_ == e1).foldLeft(g1) { + case (g2, e2) => + try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) } + catch { + case exn: Graph.Cycles[_] => + error(cat_lines(exn.cycles.map(cycle => + "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") + + " due to session " + quote(s)))) + } + } } - } } } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Admin/build_csdp.scala --- a/src/Pure/Admin/build_csdp.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Admin/build_csdp.scala Thu Mar 04 15:41:46 2021 +0100 @@ -31,7 +31,7 @@ def change_line(line: String, entry: (String, String)): String = line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2) File.change(path, s => - split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n")) + split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n")) } } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Admin/build_history.scala Thu Mar 04 15:41:46 2021 +0100 @@ -519,7 +519,7 @@ cat_lines(for ((_, log_path) <- results) yield log_path.implode)) } - val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc } + val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc } if (rc != 0 && exit_code) sys.exit(rc) } } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Admin/build_status.scala Thu Mar 04 15:41:46 2021 +0100 @@ -429,11 +429,13 @@ entry.stored_heap.toString).mkString(" ")))) val max_time = - ((0.0 /: session.finished_entries){ case (m, entry) => - m.max(entry.timing.elapsed.minutes). - max(entry.timing.resources.minutes). - max(entry.ml_timing.elapsed.minutes). - max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1 + (session.finished_entries.foldLeft(0.0) { + case (m, entry) => + m.max(entry.timing.elapsed.minutes). + max(entry.timing.resources.minutes). + max(entry.ml_timing.elapsed.minutes). + max(entry.ml_timing.resources.minutes) + } max 0.1) * 1.1 val timing_range = "[0:" + max_time + "]" def gnuplot(plot_name: String, plots: List[String], range: String): Image = diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Admin/ci_profile.scala --- a/src/Pure/Admin/ci_profile.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Admin/ci_profile.scala Thu Mar 04 15:41:46 2021 +0100 @@ -56,7 +56,7 @@ case session if group.forall(results.info(session).groups.contains(_)) => results(session).timing } - (Timing.zero /: timings)(_ + _) + timings.foldLeft(Timing.zero)(_ + _) } private def with_documents(options: Options): Options = diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Mar 04 15:41:46 2021 +0100 @@ -183,9 +183,9 @@ if (historic || items.exists(_.known_versions(rev, afp_rev))) { val longest_run = - (List.empty[Item] /: runs)({ case (item1, item2) => - if (item1.length >= item2.length) item1 else item2 - }) + runs.foldLeft(List.empty[Item]) { + case (item1, item2) => if (item1.length >= item2.length) item1 else item2 + } if (longest_run.isEmpty) None else Some(longest_run(longest_run.length / 2).versions) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/completion.scala Thu Mar 04 15:41:46 2021 +0100 @@ -32,7 +32,7 @@ { def empty(range: Text.Range): Result = Result(range, "", false, Nil) def merge(history: History, results: Option[Result]*): Option[Result] = - ((None: Option[Result]) /: results)({ + results.foldLeft(None: Option[Result]) { case (result1, None) => result1 case (None, result2) => result2 case (result1 @ Some(res1), Some(res2)) => @@ -41,7 +41,7 @@ val items = (res1.items ::: res2.items).sorted(history.ordering) Some(Result(res1.range, res1.original, false, items)) } - }) + } } sealed case class Result( @@ -78,7 +78,7 @@ } } else Nil - (empty /: content)(_ + _) + content.foldLeft(empty)(_ + _) } } @@ -356,7 +356,7 @@ def add_keywords(names: List[String]): Completion = { - val keywords1 = (keywords /: names) { case (ks, k) => if (ks(k)) ks else ks + k } + val keywords1 = names.foldLeft(keywords) { case (ks, k) => if (ks(k)) ks else ks + k } if (keywords eq keywords1) this else new Completion(keywords1, words_lex, words_map, abbrevs_lex, abbrevs_map) } @@ -386,7 +386,7 @@ } def add_abbrevs(abbrevs: List[(String, String)]): Completion = - (this /: abbrevs)(_.add_abbrev(_)) + abbrevs.foldLeft(this)(_.add_abbrev(_)) private def add_abbrev(abbrev: (String, String)): Completion = abbrev match { diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/file_watcher.scala --- a/src/Pure/General/file_watcher.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/file_watcher.scala Thu Mar 04 15:41:46 2021 +0100 @@ -105,7 +105,7 @@ key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala val remove = if (key.reset) None else Some(dir) val changed = - (Set.empty[JFile] /: events.iterator) { + events.iterator.foldLeft(Set.empty[JFile]) { case (set, event) => set + dir.toPath.resolve(event.context).toFile } (remove, changed) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/graph.scala --- a/src/Pure/General/graph.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/graph.scala Thu Mar 04 15:41:46 2021 +0100 @@ -33,10 +33,16 @@ symmetric: Boolean = false)(implicit ord: Ordering[Key]): Graph[Key, A] = { val graph1 = - (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) } + entries.foldLeft(empty[Key, A](ord)) { + case (graph, ((x, info), _)) => graph.new_node(x, info) + } val graph2 = - (graph1 /: entries) { case (graph, ((x, _), ys)) => - (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) } + entries.foldLeft(graph1) { + case (graph, ((x, _), ys)) => + ys.foldLeft(graph) { + case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) + } + } graph2 } @@ -119,8 +125,8 @@ { def reach(length: Long)(rs: Map[Key, Long], x: Key): Map[Key, Long] = if (rs.get(x) match { case Some(n) => n >= length case None => false }) rs - else ((rs + (x -> length)) /: next(x))(reach(length + count(x))) - (Map.empty[Key, Long] /: xs)(reach(0)) + else next(x).foldLeft(rs + (x -> length))(reach(length + count(x))) + xs.foldLeft(Map.empty[Key, Long])(reach(0)) } def node_height(count: Key => Long): Map[Key, Long] = reachable_length(count, imm_preds, maximals) @@ -138,7 +144,7 @@ { val (n, rs) = res if (rs.contains(x)) res - else ((n + count(x), rs + x) /: next(x))(reach) + else next(x).foldLeft((n + count(x), rs + x))(reach) } @tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys = @@ -162,7 +168,7 @@ if (r_set(x)) reached else { val (rs1, r_set1) = - if (rev) ((rs, r_set + x) /: next(x))({ case (b, a) => reach(a, b) }) + if (rev) next(x).foldLeft((rs, r_set + x)) { case (b, a) => reach(a, b) } else (next(x) :\ (rs, r_set + x))(reach) (x :: rs1, r_set1) } @@ -173,7 +179,7 @@ val (rs, r_set1) = reach(x, (Nil, r_set)) (rs :: rss, r_set1) } - ((List.empty[List[Key]], empty_keys) /: xs)(reachs) + xs.foldLeft((List.empty[List[Key]], empty_keys))(reachs) } /*immediate*/ @@ -195,12 +201,14 @@ /* minimal and maximal elements */ def minimals: List[Key] = - (List.empty[Key] /: rep) { - case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms } + rep.foldLeft(List.empty[Key]) { + case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms + } def maximals: List[Key] = - (List.empty[Key] /: rep) { - case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms } + rep.foldLeft(List.empty[Key]) { + case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms + } def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty @@ -231,11 +239,11 @@ { val (preds, succs) = get_entry(x)._2 new Graph[Key, A]( - (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x))) + succs.foldLeft(preds.foldLeft(rep - x)(del_adjacent(false, x)))(del_adjacent(true, x))) } def restrict(pred: Key => Boolean): Graph[Key, A] = - (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph } + iterator.foldLeft(this) { case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph } def exclude(pred: Key => Boolean): Graph[Key, A] = restrict(name => !pred(name)) @@ -283,7 +291,7 @@ val (_, x_set) = reachable(imm_succs, List(x)) def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] = if (x == z) (z :: path) :: ps - else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path)) + else irreducible_preds(x_set, path, z).foldLeft(ps)(paths(z :: path)) if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y) } @@ -298,7 +306,7 @@ graph } - def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_)) + def transitive_closure: Graph[Key, A] = keys_iterator.foldLeft(this)(_.transitive_step(_)) def transitive_reduction_acyclic: Graph[Key, A] = { @@ -328,7 +336,7 @@ } def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] = - (this /: xs)(_.add_edge_acyclic(_, y)) + xs.foldLeft(this)(_.add_edge_acyclic(_, y)) def topological_order: List[Key] = all_succs(minimals) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/graph_display.scala --- a/src/Pure/General/graph_display.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/graph_display.scala Thu Mar 04 15:41:46 2021 +0100 @@ -43,14 +43,15 @@ def build_graph(entries: List[Entry]): Graph = { val node = - (Map.empty[String, Node] /: entries) { + entries.foldLeft(Map.empty[String, Node]) { case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident)) } - (((empty_graph /: entries) { + entries.foldLeft( + entries.foldLeft(empty_graph) { case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content) - }) /: entries) { + }) { case (g1, ((ident, _), parents)) => - (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) } + parents.foldLeft(g1) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) } } } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/linear_set.scala Thu Mar 04 15:41:46 2021 +0100 @@ -18,7 +18,7 @@ private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map()) override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]] - def from[A](entries: IterableOnce[A]): Linear_Set[A] = (empty[A] /: entries)(_.incl(_)) + def from[A](entries: IterableOnce[A]): Linear_Set[A] = entries.foldLeft(empty[A])(_.incl(_)) override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A] private class Builder[A] extends mutable.Builder[A, Linear_Set[A]] @@ -83,7 +83,7 @@ } def append_after(hook: Option[A], elems: Iterable[A]): Linear_Set[A] = // FIXME reverse fold - ((hook, this) /: elems) { + elems.foldLeft((hook, this)) { case ((last, set), elem) => (Some(elem), set.insert_after(last, elem)) }._2 diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/mercurial.scala Thu Mar 04 15:41:46 2021 +0100 @@ -144,11 +144,11 @@ val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r val log_result = log(template = """node: {node|short} {p1node|short} {p2node|short}\n""") - (Graph.string[Unit] /: split_lines(log_result)) { + split_lines(log_result).foldLeft(Graph.string[Unit]) { case (graph, Node(x, y, z)) => val deps = List(y, z).filterNot(s => s.forall(_ == '0')) - val graph1 = (graph /: (x :: deps))(_.default_node(_, ())) - (graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) }) + val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ())) + deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) }) case (graph, _) => graph } } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/multi_map.scala --- a/src/Pure/General/multi_map.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/multi_map.scala Thu Mar 04 15:41:46 2021 +0100 @@ -17,7 +17,7 @@ def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]] def from[A, B](entries: IterableOnce[(A, B)]): Multi_Map[A, B] = - (empty[A, B] /: entries)({ case (m, (a, b)) => m.insert(a, b) }) + entries.foldLeft(empty[A, B]) { case (m, (a, b)) => m.insert(a, b) } override def newBuilder[A, B]: mutable.Builder[(A, B), Multi_Map[A, B]] = new Builder[A, B] private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]] @@ -63,7 +63,7 @@ if (this eq other) this else if (isEmpty) other else - (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) { + other.rep.iterator.foldLeft(this.asInstanceOf[Multi_Map[A, B1]]) { case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) } } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/path.scala --- a/src/Pure/General/path.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/path.scala Thu Mar 04 15:41:46 2021 +0100 @@ -146,10 +146,10 @@ def check_case_insensitive(paths: List[Path]): Unit = { val table = - (Multi_Map.empty[String, String] /: paths)({ case (tab, path) => + paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) => val name = path.expand.implode tab.insert(Word.lowercase(name), name) - }) + } val collisions = (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten if (collisions.nonEmpty) { diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/pretty.scala Thu Mar 04 15:41:46 2021 +0100 @@ -75,7 +75,7 @@ { val (line, rest) = Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts) - val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len + val len1 = (line.foldLeft(0.0) { case (l, t) => l + t.length }) max len (rest: @unchecked) match { case Break(true, _, ind) :: rest1 => body_length(Break(false, indent1 + ind, 0) :: rest1, len1) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/scan.scala Thu Mar 04 15:41:46 2021 +0100 @@ -323,9 +323,9 @@ /* auxiliary operations */ private def dest(tree: Lexicon.Tree, result: List[String]): List[String] = - (result /: tree.branches.toList) ((res, entry) => - entry match { case (_, (s, tr)) => - if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) }) + tree.branches.toList.foldLeft(result) { + case (res, (_, (s, tr))) => if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) + } private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = { @@ -390,7 +390,7 @@ new Lexicon(extend(rep, 0)) } - def ++ (elems: IterableOnce[String]): Lexicon = (this /: elems)(_ + _) + def ++ (elems: IterableOnce[String]): Lexicon = elems.foldLeft(this)(_ + _) def ++ (other: Lexicon): Lexicon = if (this eq other) this diff -r 78aa7846e91f -r d8a0e996614b src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/General/symbol.scala Thu Mar 04 15:41:46 2021 +0100 @@ -336,14 +336,14 @@ } private val symbols: List[(Symbol, Properties.T)] = - (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /: - split_lines(symbols_spec).reverse) - { case (res, No_Decl()) => res + split_lines(symbols_spec).reverse. + foldLeft((List.empty[(Symbol, Properties.T)], Set.empty[Symbol])) { + case (res, No_Decl()) => res case ((list, known), decl) => val (sym, props) = read_decl(decl) if (known(sym)) (list, known) else ((sym, props) :: list, known + sym) - })._1 + }._1 /* basic properties */ diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Isar/document_structure.scala --- a/src/Pure/Isar/document_structure.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Isar/document_structure.scala Thu Mar 04 15:41:46 2021 +0100 @@ -17,7 +17,7 @@ sealed abstract class Document { def length: Int } case class Block(name: String, text: String, body: List[Document]) extends Document - { val length: Int = (0 /: body)(_ + _.length) } + { val length: Int = body.foldLeft(0)(_ + _.length) } case class Atom(length: Int) extends Document def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean = diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Isar/keyword.scala Thu Mar 04 15:41:46 2021 +0100 @@ -160,13 +160,15 @@ val kinds1 = if (kinds eq other.kinds) kinds else if (kinds.isEmpty) other.kinds - else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } + else other.kinds.foldLeft(kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } val load_commands1 = if (load_commands eq other.load_commands) load_commands else if (load_commands.isEmpty) other.load_commands - else - (load_commands /: other.load_commands) { - case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } + else { + other.load_commands.foldLeft(load_commands) { + case (m, e) => if (m.isDefinedAt(e._1)) m else m + e + } + } new Keywords(kinds1, load_commands1) } @@ -187,7 +189,7 @@ } def add_keywords(header: Thy_Header.Keywords): Keywords = - (this /: header) { + header.foldLeft(this) { case (keywords, (name, spec)) => if (spec.kind.isEmpty) keywords + Symbol.decode(name) + Symbol.encode(name) @@ -217,13 +219,12 @@ /* lexicons */ private def make_lexicon(is_minor: Boolean): Scan.Lexicon = - (Scan.Lexicon.empty /: kinds)( - { - case (lex, (name, kind)) => - if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor) - lex + name - else lex - }) + kinds.foldLeft(Scan.Lexicon.empty) { + case (lex, (name, kind)) => + if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor) + lex + name + else lex + } lazy val minor: Scan.Lexicon = make_lexicon(true) lazy val major: Scan.Lexicon = make_lexicon(false) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Isar/line_structure.scala --- a/src/Pure/Isar/line_structure.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Isar/line_structure.scala Thu Mar 04 15:41:46 2021 +0100 @@ -45,7 +45,7 @@ else span_depth val (span_depth1, after_span_depth1, element_depth1) = - ((span_depth, after_span_depth, element_depth) /: tokens) { + tokens.foldLeft((span_depth, after_span_depth, element_depth)) { case (depths @ (x, y, z), tok) => if (tok.is_begin) (z + 2, z + 1, z + 1) else if (tok.is_end) (z + 1, z - 1, z - 1) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Thu Mar 04 15:41:46 2021 +0100 @@ -16,7 +16,7 @@ val empty: Outer_Syntax = new Outer_Syntax() - def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _) + def merge(syns: List[Outer_Syntax]): Outer_Syntax = syns.foldLeft(empty)(_ ++ _) /* string literals */ @@ -61,7 +61,7 @@ keywords + (name, kind, load_command), rev_abbrevs, language_context, has_tokens = true) def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = - (this /: keywords) { + keywords.foldLeft(this) { case (syntax, (name, spec)) => syntax + (Symbol.decode(name), spec.kind, spec.load_command) + @@ -177,8 +177,9 @@ case Some(cmd) => val name = cmd.source val offset = - (0 /: content.takeWhile(_ != cmd)) { - case (i, tok) => i + Symbol.length(tok.source) } + content.takeWhile(_ != cmd).foldLeft(0) { + case (i, tok) => i + Symbol.length(tok.source) + } val end_offset = offset + Symbol.length(name) val range = Text.Range(offset, end_offset) + 1 Command_Span.Command_Span(name, Position.Range(range)) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/ML/ml_statistics.scala Thu Mar 04 15:41:46 2021 +0100 @@ -268,7 +268,7 @@ /* content */ def maximum(field: String): Double = - (0.0 /: content)({ case (m, e) => m max e.get(field) }) + content.foldLeft(0.0) { case (m, e) => m max e.get(field) } def average(field: String): Double = { diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/command.scala Thu Mar 04 15:41:46 2021 +0100 @@ -56,8 +56,8 @@ { type Entry = (Long, XML.Elem) val empty: Results = new Results(SortedMap.empty) - def make(args: IterableOnce[Results.Entry]): Results = (empty /: args)(_ + _) - def merge(args: IterableOnce[Results]): Results = (empty /: args)(_ ++ _) + def make(args: IterableOnce[Results.Entry]): Results = args.foldLeft(empty)(_ + _) + def merge(args: IterableOnce[Results]): Results = args.foldLeft(empty)(_ ++ _) } final class Results private(private val rep: SortedMap[Long, XML.Elem]) @@ -74,7 +74,7 @@ def ++ (other: Results): Results = if (this eq other) this else if (rep.isEmpty) other - else (this /: other.iterator)(_ + _) + else other.iterator.foldLeft(this)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = @@ -92,7 +92,7 @@ { type Entry = (Long, Export.Entry) val empty: Exports = new Exports(SortedMap.empty) - def merge(args: IterableOnce[Exports]): Exports = (empty /: args)(_ ++ _) + def merge(args: IterableOnce[Exports]): Exports = args.foldLeft(empty)(_ ++ _) } final class Exports private(private val rep: SortedMap[Long, Export.Entry]) @@ -107,7 +107,7 @@ def ++ (other: Exports): Exports = if (this eq other) this else if (rep.isEmpty) other - else (this /: other.iterator)(_ + _) + else other.iterator.foldLeft(this)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = @@ -134,8 +134,8 @@ type Entry = (Markup_Index, Markup_Tree) val empty: Markups = new Markups(Map.empty) def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) - def make(args: IterableOnce[Entry]): Markups = (empty /: args)(_ + _) - def merge(args: IterableOnce[Markups]): Markups = (empty /: args)(_ ++ _) + def make(args: IterableOnce[Entry]): Markups = args.foldLeft(empty)(_ + _) + def merge(args: IterableOnce[Markups]): Markups = args.foldLeft(empty)(_ ++ _) } final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) @@ -157,7 +157,7 @@ def ++ (other: Markups): Markups = if (this eq other) this else if (rep.isEmpty) other - else (this /: other.rep.iterator)(_ + _) + else other.rep.iterator.foldLeft(this)(_ + _) def redirection_iterator: Iterator[Document_ID.Generic] = for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) @@ -295,21 +295,23 @@ case XML.Elem(Markup(Markup.STATUS, _), msgs) => if (command.span.is_theory) this else { - (this /: msgs)((state, msg) => - msg match { - case elem @ XML.Elem(markup, Nil) => - state. - add_status(markup). - add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) - case _ => - Output.warning("Ignored status message: " + msg) - state - }) + msgs.foldLeft(this) { + case (state, msg) => + msg match { + case elem @ XML.Elem(markup, Nil) => + state. + add_status(markup). + add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) + case _ => + Output.warning("Ignored status message: " + msg) + state + } + } } case XML.Elem(Markup(Markup.REPORT, atts0), msgs) => - (this /: msgs)((state, msg) => - { + msgs.foldLeft(this) { + case (state, msg) => def bad(): Unit = Output.warning("Ignored report message: " + msg) msg match { @@ -342,7 +344,7 @@ } case _ => bad(); state } - }) + } case XML.Elem(Markup(name, props), body) => props match { @@ -562,7 +564,7 @@ val core_range: Text.Range = Text.Range(0, - (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length)) + span.content.reverse.iterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length)) def source(range: Text.Range): String = range.substring(source) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/command_span.scala --- a/src/Pure/PIDE/command_span.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/command_span.scala Thu Mar 04 15:41:46 2021 +0100 @@ -74,7 +74,7 @@ def keyword_pos(start: Token.Pos): Token.Pos = kind match { case _: Command_Span => - (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_)) + content.iterator.takeWhile(tok => !tok.is_command).foldLeft(start)(_.advance(_)) case _ => start } @@ -89,7 +89,7 @@ def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content)) - def length: Int = (0 /: content)(_ + _.source.length) + def length: Int = content.foldLeft(0)(_ + _.source.length) def compact_source: (String, Span) = { diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/document.scala Thu Mar 04 15:41:46 2021 +0100 @@ -246,7 +246,7 @@ var p = pos for (command <- commands) yield { val start = p - p = (p /: command.span.content)(_.advance(_)) + p = command.span.content.foldLeft(p)(_.advance(_)) (command, start) } } @@ -385,7 +385,7 @@ def purge_suppressed: Option[Nodes] = graph.keys_iterator.filter(is_suppressed).toList match { case Nil => None - case del => Some(new Nodes((graph /: del)(_.del_node(_)))) + case del => Some(new Nodes(del.foldLeft(graph)(_.del_node(_)))) } def + (entry: (Node.Name, Node)): Nodes = @@ -393,9 +393,12 @@ val (name, node) = entry val imports = node.header.imports val graph1 = - (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty)) - val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name)) - val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name)) + imports.foldLeft(graph.default_node(name, Node.empty)) { + case (g, p) => g.default_node(p, Node.empty) + } + val graph2 = + graph1.imm_preds(name).foldLeft(graph1) { case (g, dep) => g.del_edge(dep, name) } + val graph3 = imports.foldLeft(graph2) { case (g, dep) => g.add_edge(dep, name) } new Nodes(graph3.map_node(name, _ => node)) } @@ -449,8 +452,8 @@ def purge_suppressed( versions: Map[Document_ID.Version, Version]): Map[Document_ID.Version, Version] = { - (versions /: - (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)))(_ + _) + (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)). + foldLeft(versions)(_ + _) } } @@ -567,9 +570,9 @@ private lazy val reverse_edits = edits.reverse def convert(offset: Text.Offset): Text.Offset = - (offset /: edits)((i, edit) => edit.convert(i)) + edits.foldLeft(offset) { case (i, edit) => edit.convert(i) } def revert(offset: Text.Offset): Text.Offset = - (offset /: reverse_edits)((i, edit) => edit.revert(i)) + reverse_edits.foldLeft(offset) { case (i, edit) => edit.revert(i) } def convert(range: Text.Range): Text.Range = range.map(convert) def revert(range: Text.Range): Text.Range = range.map(revert) @@ -683,7 +686,7 @@ node.commands.iterator.takeWhile(_ != command).map(_.source) ++ (if (offset == 0) Iterator.empty else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset))))) - val pos = (Line.Position.zero /: sources_iterator)(_.advance(_)) + val pos = sources_iterator.foldLeft(Line.Position.zero)(_.advance(_)) Line.Node_Position(name, pos) } @@ -842,7 +845,7 @@ { require(!is_finished, "assignment already finished") val command_execs1 = - (command_execs /: update) { + update.foldLeft(command_execs) { case (res, (command_id, exec_ids)) => if (exec_ids.isEmpty) res - command_id else res + (command_id -> exec_ids) @@ -928,8 +931,10 @@ } private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] = - (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) => - graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) }) + st.markups.redirection_iterator.foldLeft(commands_redirection) { + case (graph, id) => + graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) + } def accumulate(id: Document_ID.Generic, message: XML.Elem, cache: XML.Cache) : (Command.State, State) = @@ -1022,7 +1027,7 @@ if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st) val (changed_commands, new_execs) = - ((Nil: List[Command], execs) /: update) { + update.foldLeft((Nil: List[Command], execs)) { case ((commands1, execs1), (command_id, exec)) => val st = the_static_state(command_id) val command = st.command @@ -1250,10 +1255,10 @@ } yield edits val edits = - (pending_edits /: rev_pending_changes)({ + rev_pending_changes.foldLeft(pending_edits) { case (edits, Node.Edits(es)) => es ::: edits case (edits, _) => edits - }) + } new Snapshot(this, version, node_name, edits, snippet_command) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/document_status.scala --- a/src/Pure/PIDE/document_status.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/document_status.scala Thu Mar 04 15:41:46 2021 +0100 @@ -60,7 +60,7 @@ def merge(status_iterator: Iterator[Command_Status]): Command_Status = if (status_iterator.hasNext) { val status0 = status_iterator.next() - (status0 /: status_iterator)(_ + _) + status_iterator.foldLeft(status0)(_ + _) } else empty } @@ -198,10 +198,10 @@ st <- state.command_states(version, command) } { val command_timing = - (0.0 /: st.status)({ + st.status.foldLeft(0.0) { case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds case (timing, _) => timing - }) + } total += command_timing if (command_timing > 0.0 && command_timing >= threshold) { command_timings += (command -> command_timing) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/headless.scala Thu Mar 04 15:41:46 2021 +0100 @@ -154,7 +154,8 @@ if (add.isEmpty) front else { val preds = add.map(dep_graph.imm_preds) - val base1 = (preds.head /: preds.tail)(_ ++ _).toList.filter(already_committed.keySet) + val base1 = + preds.tail.foldLeft(preds.head)(_ ++ _).toList.filter(already_committed.keySet) frontier(base1, front ++ add) } } @@ -182,21 +183,21 @@ commit match { case None => already_committed case Some(commit_fn) => - (already_committed /: dep_graph.topological_order)( - { case (committed, name) => - def parents_committed: Boolean = - version.nodes(name).header.imports.forall(parent => - loaded_theory(parent) || committed.isDefinedAt(parent)) - if (!committed.isDefinedAt(name) && parents_committed && - state.node_consolidated(version, name)) - { - val snapshot = stable_snapshot(state, version, name) - val status = Document_Status.Node_Status.make(state, version, name) - commit_fn(snapshot, status) - committed + (name -> status) - } - else committed - }) + dep_graph.topological_order.foldLeft(already_committed) { + case (committed, name) => + def parents_committed: Boolean = + version.nodes(name).header.imports.forall(parent => + loaded_theory(parent) || committed.isDefinedAt(parent)) + if (!committed.isDefinedAt(name) && parents_committed && + state.node_consolidated(version, name)) + { + val snapshot = stable_snapshot(state, version, name) + val status = Document_Status.Node_Status.make(state, version, name) + commit_fn(snapshot, status) + committed + (name -> status) + } + else committed + } } def finished_theory(name: Document.Node.Name): Boolean = @@ -472,8 +473,8 @@ case None => Some(name -> new_blob) } }) - val blobs1 = (blobs /: new_blobs)(_ + _) - val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) }) + val blobs1 = new_blobs.foldLeft(blobs)(_ + _) + val blobs2 = new_blobs.foldLeft(blobs) { case (map, (a, b)) => map + (a -> b.unchanged) } (Document.Blobs(blobs1), copy(blobs = blobs2)) } @@ -501,19 +502,20 @@ def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) def insert_required(id: UUID.T, names: List[Document.Node.Name]): State = - copy(required = (required /: names)(_.insert(_, id))) + copy(required = names.foldLeft(required)(_.insert(_, id))) def remove_required(id: UUID.T, names: List[Document.Node.Name]): State = - copy(required = (required /: names)(_.remove(_, id))) + copy(required = names.foldLeft(required)(_.remove(_, id))) def update_theories(update: List[(Document.Node.Name, Theory)]): State = copy(theories = - (theories /: update)({ case (thys, (name, thy)) => - thys.get(name) match { - case Some(thy1) if thy1 == thy => thys - case _ => thys + (name -> thy) - } - })) + update.foldLeft(theories) { + case (thys, (name, thy)) => + thys.get(name) match { + case Some(thy1) if thy1 == thy => thys + case _ => thys + (name -> thy) + } + }) def remove_theories(remove: List[Document.Node.Name]): State = { diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/line.scala Thu Mar 04 15:41:46 2021 +0100 @@ -118,7 +118,7 @@ private def length(lines: List[Line]): Int = if (lines.isEmpty) 0 - else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1 + else (lines.foldLeft(0) { case (n, line) => n + line.text.length + 1 }) - 1 def text(lines: List[Line]): String = lines.mkString("", "\n", "") } @@ -169,7 +169,7 @@ if (0 <= l && l < n) { if (0 <= c && c <= lines(l).text.length) { val line_offset = - (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 } + lines.iterator.take(l).foldLeft(0) { case (n, line) => n + line.text.length + 1 } Some(line_offset + c) } else None diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/markup_tree.scala Thu Mar 04 15:41:46 2021 +0100 @@ -20,16 +20,16 @@ val empty: Markup_Tree = new Markup_Tree(Branches.empty) def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree = - (empty /: trees)(_.merge(_, range, elements)) + trees.foldLeft(empty)(_.merge(_, range, elements)) def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree = trees match { case Nil => empty case head :: tail => new Markup_Tree( - (head.branches /: tail) { + tail.foldLeft(head.branches) { case (branches, tree) => - (branches /: tree.branches) { + tree.branches.foldLeft(branches) { case (bs, (r, entry)) => require(!bs.isDefinedAt(r), "cannot merge markup trees") bs + (r -> entry) @@ -93,7 +93,8 @@ (offset + XML.text_length(body), markup_trees) case (elems, body) => - val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees) + val (end_offset, subtrees) = + body.foldLeft((offset, Nil: List[Markup_Tree]))(make_trees) if (offset == end_offset) acc else { val range = Text.Range(offset, end_offset) @@ -104,7 +105,7 @@ } def from_XML(body: XML.Body): Markup_Tree = - merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2) + merge_disjoint(body.foldLeft((0, Nil: List[Markup_Tree]))(make_trees)._2) } @@ -163,13 +164,15 @@ def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree = { def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree = - (tree1 /: tree2.branches)( - { case (tree, (range, entry)) => - if (!range.overlaps(root_range)) tree - else - (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))( - { case (t, elem) => t + Text.Info(range, elem) }) - }) + tree2.branches.foldLeft(tree1) { + case (tree, (range, entry)) => + if (!range.overlaps(root_range)) tree + else { + entry.filter_markup(elements).foldLeft(merge_trees(tree, entry.subtree)) { + case (t, elem) => t + Text.Info(range, elem) + } + } + } if (this eq other) this else { @@ -236,7 +239,7 @@ else List(XML.Text(text.subSequence(start, stop).toString)) def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body = - (body /: rev_markups) { + rev_markups.foldLeft(body) { case (b, elem) => if (!elements(elem.name)) b else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b)) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/protocol_handlers.scala --- a/src/Pure/PIDE/protocol_handlers.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/protocol_handlers.scala Thu Mar 04 15:41:46 2021 +0100 @@ -74,8 +74,9 @@ private val state = Synchronized(Protocol_Handlers.State(session)) def prover_options(options: Options): Options = - (options /: state.value.handlers)( - { case (opts, (_, handler)) => handler.prover_options(opts) }) + state.value.handlers.foldLeft(options) { + case (opts, (_, handler)) => handler.prover_options(opts) + } def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name) def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler)) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/prover.scala Thu Mar 04 15:41:46 2021 +0100 @@ -349,7 +349,7 @@ command_input match { case Some(thread) if thread.is_active => if (trace) { - val payload = (0 /: args)({ case (n, b) => n + b.length }) + val payload = args.foldLeft(0) { case (n, b) => n + b.length } Output.writeln( "protocol_command " + name + ", args = " + args.length + ", payload = " + payload) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/rendering.scala Thu Mar 04 15:41:46 2021 +0100 @@ -177,7 +177,7 @@ def apply(ids: Set[Long]): Focus = new Focus(ids) val empty: Focus = apply(Set.empty) def make(args: List[Text.Info[Focus]]): Focus = - (empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }) + args.foldLeft(empty) { case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 } val full: Focus = new Focus(Set.empty) @@ -195,7 +195,7 @@ def ++ (other: Focus): Focus = if (this eq other) this else if (rep.isEmpty) other - else (this /: other.rep.iterator)(_ + _) + else other.rep.iterator.foldLeft(this)(_ + _) override def toString: String = rep.mkString("Focus(", ",", ")") } @@ -709,7 +709,7 @@ else { val r = Text.Range(results.head.range.start, results.last.range.stop) val all_tips = - (SortedMap.empty[Long, XML.Tree] /: results.flatMap(_.messages))(_ + _) + results.flatMap(_.messages).foldLeft(SortedMap.empty[Long, XML.Tree])(_ + _) .iterator.map(_._2).toList ::: results.flatMap(res => res.infos(true)) ::: results.flatMap(res => res.infos(false)).lastOption.toList diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/resources.scala Thu Mar 04 15:41:46 2021 +0100 @@ -291,11 +291,12 @@ def session_dependencies(info: Sessions.Info, progress: Progress = new Progress) : Dependencies[Options] = { - (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) => - dependencies.require_thys(options, - for { (thy, pos) <- thys } yield (import_name(info, thy), pos), - progress = progress) - }) + info.theories.foldLeft(Dependencies.empty[Options]) { + case (dependencies, (options, thys)) => + dependencies.require_thys(options, + for { (thy, pos) <- thys } yield (import_name(info, thy), pos), + progress = progress) + } } object Dependencies @@ -361,7 +362,7 @@ thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress, initiators: List[Document.Node.Name] = Nil): Dependencies[A] = - (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators)) + thys.foldLeft(this)(_.require_thy(adjunct, _, progress = progress, initiators = initiators)) def entries: List[Document.Node.Entry] = rev_entries.reverse @@ -392,19 +393,20 @@ } lazy val loaded_theories: Graph[String, Outer_Syntax] = - (session_base.loaded_theories /: entries)({ case (graph, entry) => - val name = entry.name.theory - val imports = entry.header.imports.map(_.theory) - - val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty)) - val graph2 = (graph1 /: imports)(_.add_edge(_, name)) + entries.foldLeft(session_base.loaded_theories) { + case (graph, entry) => + val name = entry.name.theory + val imports = entry.header.imports.map(_.theory) - val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil - val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node) - val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header + val graph1 = (name :: imports).foldLeft(graph)(_.default_node(_, Outer_Syntax.empty)) + val graph2 = imports.foldLeft(graph1)(_.add_edge(_, name)) - graph2.map_node(name, _ => syntax) - }) + val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil + val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node) + val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header + + graph2.map_node(name, _ => syntax) + } def get_syntax(name: Document.Node.Name): Outer_Syntax = loaded_theories.get_node(name.theory) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/PIDE/xml.scala Thu Mar 04 15:41:46 2021 +0100 @@ -101,11 +101,11 @@ { def traverse(x: A, t: Tree): A = t match { - case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse) - case XML.Elem(_, ts) => (x /: ts)(traverse) + case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse) + case XML.Elem(_, ts) => ts.foldLeft(x)(traverse) case XML.Text(s) => op(x, s) } - (a /: body)(traverse) + body.foldLeft(a)(traverse) } def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/System/getopts.scala --- a/src/Pure/System/getopts.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/System/getopts.scala Thu Mar 04 15:41:46 2021 +0100 @@ -15,7 +15,7 @@ def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts = { val options = - (Map.empty[Char, (Boolean, String => Unit)] /: option_specs) { + option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) { case (m, (s, f)) => val (a, entry) = if (s.size == 1) (s(0), (false, f)) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/System/options.scala --- a/src/Pure/System/options.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/System/options.scala Thu Mar 04 15:41:46 2021 +0100 @@ -119,7 +119,7 @@ case Success(result, _) => result case bad => error(bad.toString) } - try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } } + try { ops.foldLeft(options.set_section("")) { case (opts, op) => op(opts) } } catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) } } @@ -137,7 +137,7 @@ dir <- Isabelle_System.components() file = dir + OPTIONS if file.is_file } { options = Parser.parse_file(options, file.implode, File.read(file)) } - (Options.Parser.parse_prefs(options, prefs) /: opts)(_ + _) + opts.foldLeft(Options.Parser.parse_prefs(options, prefs))(_ + _) } @@ -181,9 +181,9 @@ val options0 = Options.init() val options1 = if (build_options) - (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _) + Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _) else options0 - (options1 /: more_options)(_ + _) + more_options.foldLeft(options1)(_ + _) } if (get_option != "") @@ -363,7 +363,7 @@ } def ++ (specs: List[Options.Spec]): Options = - (this /: specs)({ case (x, (y, z)) => x + (y, z) }) + specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) } /* sections */ diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Thy/bibtex.scala Thu Mar 04 15:41:46 2021 +0100 @@ -389,7 +389,9 @@ def heading_length: Int = if (name == "") 1 - else (0 /: tokens.takeWhile(tok => !tok.is_open)){ case (n, tok) => n + tok.source.length } + else { + tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length } + } def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored) def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Thy/export_theory.scala Thu Mar 04 15:41:46 2021 +0100 @@ -48,12 +48,16 @@ })) val graph0 = - (Graph.string[Option[Theory]] /: thys) { - case (g, thy) => g.default_node(thy.name, Some(thy)) } + thys.foldLeft(Graph.string[Option[Theory]]) { + case (g, thy) => g.default_node(thy.name, Some(thy)) + } val graph1 = - (graph0 /: thys) { case (g0, thy) => - (g0 /: thy.parents) { case (g1, parent) => - g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } } + thys.foldLeft(graph0) { + case (g0, thy) => + thy.parents.foldLeft(g0) { + case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) + } + } Session(session_name, graph1) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/file_format.scala --- a/src/Pure/Thy/file_format.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Thy/file_format.scala Thu Mar 04 15:41:46 2021 +0100 @@ -39,7 +39,7 @@ agents.mkString("File_Format.Session(", ", ", ")") def prover_options(options: Options): Options = - (options /: agents)({ case (opts, agent) => agent.prover_options(opts) }) + agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) } def stop_session: Unit = agents.foreach(_.stop) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Thy/latex.scala Thu Mar 04 15:41:46 2021 +0100 @@ -67,8 +67,8 @@ case None => None case Some(file) => val source_line = - (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))( - { case (_, (_, n)) => n }) + source_lines.iterator.takeWhile({ case (m, _) => m <= l }). + foldLeft(0) { case (_, (_, n)) => n } if (source_line == 0) None else Some(Position.Line_File(source_line, file)) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Thy/sessions.scala Thu Mar 04 15:41:46 2021 +0100 @@ -156,7 +156,7 @@ } val session_bases = - (Map("" -> sessions_structure.bootstrap) /: sessions_structure.imports_topological_order)({ + sessions_structure.imports_topological_order.foldLeft(Map("" -> sessions_structure.bootstrap)) { case (session_bases, session_name) => progress.expose_interrupt() @@ -230,22 +230,24 @@ .transitive_reduction_acyclic val graph0 = - (Graph_Display.empty_graph /: required_subgraph.topological_order)( - { case (g, session) => - val a = session_node(session) - val bs = required_subgraph.imm_preds(session).toList.map(session_node) - ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) + required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) { + case (g, session) => + val a = session_node(session) + val bs = required_subgraph.imm_preds(session).toList.map(session_node) + bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a)) + } - (graph0 /: dependencies.entries)( - { case (g, entry) => - val a = node(entry.name) - val bs = entry.header.imports.map(node).filterNot(_ == a) - ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) + dependencies.entries.foldLeft(graph0) { + case (g, entry) => + val a = node(entry.name) + val bs = entry.header.imports.map(node).filterNot(_ == a) + bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a)) + } } val known_theories = - (deps_base.known_theories /: - dependencies.entries.iterator.map(entry => entry.name.theory -> entry))(_ + _) + dependencies.entries.iterator.map(entry => entry.name.theory -> entry). + foldLeft(deps_base.known_theories)(_ + _) val known_loaded_files = deps_base.known_loaded_files ++ loaded_files @@ -357,7 +359,7 @@ cat_error(msg, "The error(s) above occurred in session " + quote(info.name) + Position.here(info.pos)) } - }) + } Deps(sessions_structure, session_bases) } @@ -489,14 +491,13 @@ val imports_bases = imports.map(session_bases) parent_base.copy( known_theories = - (parent_base.known_theories /: - (for { - base <- imports_bases.iterator - (_, entry) <- base.known_theories.iterator - } yield (entry.name.theory -> entry)))(_ + _), + (for { + base <- imports_bases.iterator + (_, entry) <- base.known_theories.iterator + } yield (entry.name.theory -> entry)).foldLeft(parent_base.known_theories)(_ + _), known_loaded_files = - (parent_base.known_loaded_files /: - imports_bases.iterator.map(_.known_loaded_files))(_ ++ _)) + imports_bases.iterator.map(_.known_loaded_files). + foldLeft(parent_base.known_loaded_files)(_ ++ _)) } def dirs: List[Path] = dir :: directories @@ -661,13 +662,14 @@ cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos)) } } - (graph /: graph.iterator) { - case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _)) + graph.iterator.foldLeft(graph) { + case (g, (name, (info, _))) => + edges(info).foldLeft(g)(add_edge(info.pos, name, _, _)) } } val info_graph = - (Graph.string[Info] /: infos) { + infos.foldLeft(Graph.string[Info]) { case (graph, info) => if (graph.defined(info.name)) error("Duplicate session " + quote(info.name) + Position.here(info.pos) + @@ -681,12 +683,12 @@ (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList val session_directories: Map[JFile, String] = - (Map.empty[JFile, String] /: - (for { - session <- imports_graph.topological_order.iterator - info = info_graph.get_node(session) - dir <- info.dirs.iterator - } yield (info, dir)))({ case (dirs, (info, dir)) => + (for { + session <- imports_graph.topological_order.iterator + info = info_graph.get_node(session) + dir <- info.dirs.iterator + } yield (info, dir)).foldLeft(Map.empty[JFile, String]) { + case (dirs, (info, dir)) => val session = info.name val canonical_dir = dir.canonical_file dirs.get(canonical_dir) match { @@ -697,22 +699,22 @@ "\n vs. session " + quote(session) + Position.here(info.pos)) case None => dirs + (canonical_dir -> session) } - }) + } val global_theories: Map[String, String] = - (Thy_Header.bootstrap_global_theories.toMap /: - (for { - session <- imports_graph.topological_order.iterator - info = info_graph.get_node(session) - thy <- info.global_theories.iterator } - yield (info, thy)))({ case (global, (info, thy)) => + (for { + session <- imports_graph.topological_order.iterator + info = info_graph.get_node(session) + thy <- info.global_theories.iterator } + yield (info, thy)).foldLeft(Thy_Header.bootstrap_global_theories.toMap) { + case (global, (info, thy)) => val qualifier = info.name global.get(thy) match { case Some(qualifier1) if qualifier != qualifier1 => error("Duplicate global theory " + quote(thy) + Position.here(info.pos)) case _ => global + (thy -> qualifier) } - }) + } new Structure( session_positions, session_directories, global_theories, build_graph, imports_graph) @@ -739,9 +741,10 @@ yield (File.standard_path(file), session) lazy val chapters: SortedMap[String, List[Info]] = - (SortedMap.empty[String, List[Info]] /: build_graph.iterator)( - { case (chs, (_, (info, _))) => - chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) }) + build_graph.iterator.foldLeft(SortedMap.empty[String, List[Info]]) { + case (chs, (_, (info, _))) => + chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) + } def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph) def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph) @@ -1061,13 +1064,14 @@ } yield res val unique_roots = - ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) => - val file = path.canonical_file - m.get(file) match { - case None => m + (file -> (select, path)) - case Some((select1, path1)) => m + (file -> (select1 || select, path1)) - } - }).toList.map(_._2) + roots.foldLeft(Map.empty[JFile, (Boolean, Path)]) { + case (m, (select, path)) => + val file = path.canonical_file + m.get(file) match { + case None => m + (file -> (select, path)) + case Some((select1, path1)) => m + (file -> (select1 || select, path1)) + } + }.toList.map(_._2) Structure.make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Thy/thy_header.scala Thu Mar 04 15:41:46 2021 +0100 @@ -223,7 +223,7 @@ val (skip_tokens, tokens) = read_tokens(Scan.char_reader(text), strict) val pos = if (command) Token.Pos.command - else (Token.Pos.file(node_name.node) /: skip_tokens)(_ advance _) + else skip_tokens.foldLeft(Token.Pos.file(node_name.node))(_ advance _) Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name) } diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Thu Mar 04 15:41:46 2021 +0100 @@ -191,7 +191,7 @@ val inserted = blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), node_name, blobs, span) }) - (commands /: cmds2)(_ - _).append_after(hook, inserted) + cmds2.foldLeft(commands)(_ - _).append_after(hook, inserted) } } @@ -310,12 +310,12 @@ if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes)) else { val reparse = - (syntax_changed /: nodes0.iterator)({ + nodes0.iterator.foldLeft(syntax_changed) { case (reparse, (name, node)) => if (node.load_commands_changed(doc_blobs) && !reparse.contains(name)) name :: reparse else reparse - }) + } val reparse_set = reparse.toSet var nodes = nodes0 @@ -338,7 +338,7 @@ commands, commands.head, commands.last)) else node val node2 = - (node1 /: edits)( + edits.foldLeft(node1)( text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _)) val node3 = if (reparse_set.contains(name)) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Tools/build.scala Thu Mar 04 15:41:46 2021 +0100 @@ -159,8 +159,8 @@ def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1)) def info(name: String): Sessions.Info = results(name)._2 val rc: Int = - (0 /: results.iterator.map( - { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _) + results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }). + foldLeft(0)(_ max _) def ok: Boolean = rc == 0 override def toString: String = rc.toString @@ -661,7 +661,7 @@ } val total_timing = - (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). + results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Tools/dump.scala Thu Mar 04 15:41:46 2021 +0100 @@ -105,7 +105,7 @@ "completion_limit=0" + "editor_tracing_messages=0" + "editor_presentation" - (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) + aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) } } val sessions_structure: Sessions.Structure = diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Tools/scala_project.scala --- a/src/Pure/Tools/scala_project.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Tools/scala_project.scala Thu Mar 04 15:41:46 2021 +0100 @@ -53,7 +53,7 @@ } lazy val isabelle_scala_files: Map[String, Path] = - (Map.empty[String, Path] /: isabelle_files)({ + isabelle_files.foldLeft(Map.empty[String, Path]) { case (map, name) => if (!name.startsWith("src/Tools/jEdit/") && name.endsWith(".scala")) { val path = Path.explode("~~/" + name) @@ -64,7 +64,7 @@ } } else map - }) + } val isabelle_dirs: List[(String, Path)] = List( diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/Tools/server.scala Thu Mar 04 15:41:46 2021 +0100 @@ -74,12 +74,13 @@ } private lazy val command_table: Map[String, Command] = - (Map.empty[String, Command] /: Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries))( - { case (cmds, cmd) => + Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries). + foldLeft(Map.empty[String, Command]) { + case (cmds, cmd) => val name = cmd.command_name if (cmds.isDefinedAt(name)) error("Duplicate Isabelle server command: " + quote(name)) else cmds + (name -> cmd) - }) + } /* output reply */ diff -r 78aa7846e91f -r d8a0e996614b src/Tools/Graphview/layout.scala --- a/src/Tools/Graphview/layout.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/Graphview/layout.scala Thu Mar 04 15:41:46 2021 +0100 @@ -108,10 +108,10 @@ }).toList) val initial_levels: Levels = - (empty_levels /: initial_graph.topological_order) { + initial_graph.topological_order.foldLeft(empty_levels) { case (levels, vertex) => val level = - 1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) } + 1 + initial_graph.imm_preds(vertex).foldLeft(-1) { case (m, v) => m max levels(v) } levels + (vertex -> level) } @@ -121,25 +121,26 @@ val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil) val (dummy_graph, dummy_levels) = - ((initial_graph, initial_levels) /: input_graph.edges_iterator) { - case ((graph, levels), (node1, node2)) => - val v1 = Node(node1); val l1 = levels(v1) - val v2 = Node(node2); val l2 = levels(v2) - if (l2 - l1 <= 1) (graph, levels) - else { - val dummies_levels = - (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex } - yield (Dummy(node1, node2, i), l)).toList - val dummies = dummies_levels.map(_._1) + input_graph.edges_iterator.foldLeft((initial_graph, initial_levels)) { + case ((graph, levels), (node1, node2)) => + val v1 = Node(node1); val l1 = levels(v1) + val v2 = Node(node2); val l2 = levels(v2) + if (l2 - l1 <= 1) (graph, levels) + else { + val dummies_levels = + (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex } + yield (Dummy(node1, node2, i), l)).toList + val dummies = dummies_levels.map(_._1) - val levels1 = (levels /: dummies_levels)(_ + _) - val graph1 = - ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /: - (v1 :: dummies ::: List(v2)).sliding(2)) { - case (g, List(a, b)) => g.add_edge(a, b) } - (graph1, levels1) - } - } + val levels1 = dummies_levels.foldLeft(levels)(_ + _) + val graph1 = + (v1 :: dummies ::: List(v2)).sliding(2). + foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) { + case (g, List(a, b)) => g.add_edge(a, b) + } + (graph1, levels1) + } + } /* minimize edge crossings and initial coordinates */ @@ -147,25 +148,26 @@ val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels)) val levels_graph: Graph = - (((dummy_graph, 0.0) /: levels) { + levels.foldLeft((dummy_graph, 0.0)) { case ((graph, y), level) => - val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length } - val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size } + val num_lines = level.foldLeft(0) { case (n, v) => n max graph.get_node(v).lines.length } + val num_edges = level.foldLeft(0) { case (n, v) => n + graph.imm_succs(v).size } val y1 = y + metrics.node_height2(num_lines) val graph1 = - (((graph, 0.0) /: level) { case ((g, x), v) => - val info = g.get_node(v) - val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1)) - val x1 = x + info.width + metrics.gap - (g1, x1) - })._1 + level.foldLeft((graph, 0.0)) { + case ((g, x), v) => + val info = g.get_node(v) + val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1)) + val x1 = x + info.width + metrics.gap + (g1, x1) + }._1 val y2 = y1 + metrics.level_height2(num_lines, num_edges) (graph1, y2) - })._1 + }._1 /* pendulum/rubberband layout */ @@ -188,37 +190,41 @@ options: Options, graph: Graph, levels: List[Level]): List[Level] = { def resort(parent: Level, child: Level, top_down: Boolean): Level = - child.map(v => { - val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v) - val weight = - (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) - (v, weight) + child.map(v => + { + val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v) + val weight = + ps.foldLeft(0.0) { case (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) + (v, weight) }).sortBy(_._2).map(_._1) - ((levels, count_crossings(graph, levels)) /: - (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) { - case ((old_levels, old_crossings), iteration) => - val top_down = (iteration % 2 == 1) - val new_levels = - if (top_down) - (List(old_levels.head) /: old_levels.tail)((tops, bot) => - resort(tops.head, bot, top_down) :: tops).reverse - else { - val rev_old_levels = old_levels.reverse - (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) => - resort(bots.head, top, top_down) :: bots) - } - val new_crossings = count_crossings(graph, new_levels) - if (new_crossings < old_crossings) - (new_levels, new_crossings) - else - (old_levels, old_crossings) - }._1 + (1 to (2 * options.int("graphview_iterations_minimize_crossings"))). + foldLeft((levels, count_crossings(graph, levels))) { + case ((old_levels, old_crossings), iteration) => + val top_down = (iteration % 2 == 1) + val new_levels = + if (top_down) { + old_levels.tail.foldLeft(List(old_levels.head)) { + case (tops, bot) => resort(tops.head, bot, top_down) :: tops + }.reverse + } + else { + val rev_old_levels = old_levels.reverse + rev_old_levels.tail.foldLeft(List(rev_old_levels.head)) { + case (bots, top) => resort(bots.head, top, top_down) :: bots + } + } + val new_crossings = count_crossings(graph, new_levels) + if (new_crossings < old_crossings) + (new_levels, new_crossings) + else + (old_levels, old_crossings) + }._1 } private def level_list(levels: Levels): List[Level] = { - val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l } + val max_lev = levels.foldLeft(-1) { case (m, (_, l)) => m max l } val buckets = new Array[Level](max_lev + 1) for (l <- 0 to max_lev) { buckets(l) = Nil } for ((v, l) <- levels) { buckets(l) = v :: buckets(l) } @@ -260,7 +266,7 @@ }).sum / content.length).round.toDouble def move(graph: Graph, dx: Double): Graph = - if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx)) + if (dx == 0.0) graph else content.foldLeft(graph)(move_vertex(_, _, dx)) def combine(that: Region): Region = new Region(content ::: that.content) } @@ -289,7 +295,7 @@ def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) = { - ((graph, false) /: level.indices) { + level.indices.foldLeft((graph, false)) { case ((graph, moved), i) => val r = level(i) val d = r.deflection(graph, top_down) @@ -307,22 +313,23 @@ val initial_regions = levels.map(level => level.map(l => new Region(List(l)))) - ((levels_graph, initial_regions, true) /: - (1 to (2 * options.int("graphview_iterations_pendulum")))) { - case ((graph, regions, moved), iteration) => - val top_down = (iteration % 2 == 1) - if (moved) { - val (graph1, regions1, moved1) = - ((graph, List.empty[List[Region]], false) /: - (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) => - val bot1 = combine_regions(graph, top_down, bot) - val (graph1, moved1) = deflect(bot1, top_down, graph) - (graph1, bot1 :: tops, moved || moved1) - } - (graph1, regions1.reverse, moved1) - } - else (graph, regions, moved) - }._1 + (1 to (2 * options.int("graphview_iterations_pendulum"))). + foldLeft((levels_graph, initial_regions, true)) { + case ((graph, regions, moved), iteration) => + val top_down = (iteration % 2 == 1) + if (moved) { + val (graph1, regions1, moved1) = + (if (top_down) regions else regions.reverse). + foldLeft((graph, List.empty[List[Region]], false)) { + case ((graph, tops, moved), bot) => + val bot1 = combine_regions(graph, top_down, bot) + val (graph1, moved1) = deflect(bot1, top_down, graph) + (graph1, bot1 :: tops, moved || moved1) + } + (graph1, regions1.reverse, moved1) + } + else (graph, regions, moved) + }._1 } @@ -346,18 +353,19 @@ { val gap = metrics.gap - (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) => - (graph /: levels) { case (graph, level) => - val m = level.length - 1 - (graph /: level.iterator.zipWithIndex) { - case (g, (v, i)) => - val d = force_weight(g, v) - if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) || - d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d)) - move_vertex(g, v, d.round.toDouble) - else g + (1 to (2 * options.int("graphview_iterations_rubberband"))).foldLeft(graph) { + case (graph, _) => + levels.foldLeft(graph) { case (graph, level) => + val m = level.length - 1 + level.iterator.zipWithIndex.foldLeft(graph) { + case (g, (v, i)) => + val d = force_weight(g, v) + if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) || + d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d)) + move_vertex(g, v, d.round.toDouble) + else g + } } - } } } } diff -r 78aa7846e91f -r d8a0e996614b src/Tools/Graphview/metrics.scala --- a/src/Tools/Graphview/metrics.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/Graphview/metrics.scala Thu Mar 04 15:41:46 2021 +0100 @@ -46,7 +46,8 @@ def dummy_size2: Double = (char_width / 2).ceil def node_width2(lines: List[String]): Double = - (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil + ((lines.foldLeft(0.0)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2) + .ceil def node_height2(num_lines: Int): Double = ((height.ceil * (num_lines max 1) + char_width) / 2).ceil diff -r 78aa7846e91f -r d8a0e996614b src/Tools/Graphview/model.scala --- a/src/Tools/Graphview/model.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/Graphview/model.scala Thu Mar 04 15:41:46 2021 +0100 @@ -54,7 +54,7 @@ full_graph.keys_iterator.find(node => node.ident == ident) def make_visible_graph(): Graph_Display.Graph = - (full_graph /: Mutators()) { + Mutators().foldLeft(full_graph) { case (g, m) => if (!m.enabled) g else m.mutator.mutate(full_graph, g) } @@ -64,9 +64,9 @@ private def build_colors(): Unit = { _colors = - (Map.empty[Graph_Display.Node, Color] /: Colors()) { + Colors().foldLeft(Map.empty[Graph_Display.Node, Color]) { case (colors, m) => - (colors /: m.mutator.mutate(full_graph, full_graph).keys_iterator) { + m.mutator.mutate(full_graph, full_graph).keys_iterator.foldLeft(colors) { case (colors, node) => colors + (node -> m.color) } } diff -r 78aa7846e91f -r d8a0e996614b src/Tools/Graphview/mutator.scala --- a/src/Tools/Graphview/mutator.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/Graphview/mutator.scala Thu Mar 04 15:41:46 2021 +0100 @@ -51,10 +51,11 @@ extends Graph_Filter( name, description, - g => (g /: g.dest) { + g => g.dest.foldLeft(g) { case (graph, ((from, _), tos)) => - (graph /: tos)((gr, to) => - if (pred(gr, (from, to))) gr else gr.del_edge(from, to)) + tos.foldLeft(graph) { + case (gr, to) => if (pred(gr, (from, to))) gr else gr.del_edge(from, to) + } }) class Node_Family_Filter( @@ -116,26 +117,24 @@ { // Add Nodes val with_nodes = - (to /: keys)((graph, key) => graph.default_node(key, from.get_node(key))) + keys.foldLeft(to) { case (graph, key) => graph.default_node(key, from.get_node(key)) } // Add Edges - (with_nodes /: keys) { - (gv, key) => { + keys.foldLeft(with_nodes) { + case (gv, key) => def add_edges(g: Graph_Display.Graph, keys: from.Keys, succs: Boolean) = - (g /: keys) { - (graph, end) => { + keys.foldLeft(g) { + case (graph, end) => if (!graph.keys_iterator.contains(end)) graph else { if (succs) graph.add_edge(key, end) else graph.add_edge(end, key) } - } } add_edges( add_edges(gv, from.imm_preds(key), false), from.imm_succs(key), true) - } } } diff -r 78aa7846e91f -r d8a0e996614b src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/Graphview/shapes.scala Thu Mar 04 15:41:46 2021 +0100 @@ -55,7 +55,7 @@ gfx.setFont(metrics.font) val text_width = - (0.0 /: info.lines) { case (w, line) => w max metrics.string_bounds(line).getWidth } + info.lines.foldLeft(0.0) { case (w, line) => w max metrics.string_bounds(line).getWidth } val text_height = (info.lines.length max 1) * metrics.height.ceil val x = (s.getCenterX - text_width / 2).round.toInt @@ -126,7 +126,7 @@ val dy = coords(2).y - coords(0).y val (dx2, dy2) = - ((dx, dy) /: coords.sliding(3)) { + coords.sliding(3).foldLeft((dx, dy)) { case ((dx, dy), List(l, m, r)) => val dx2 = r.x - l.x val dy2 = r.y - l.y diff -r 78aa7846e91f -r d8a0e996614b src/Tools/VSCode/src/preview_panel.scala --- a/src/Tools/VSCode/src/preview_panel.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/VSCode/src/preview_panel.scala Thu Mar 04 15:41:46 2021 +0100 @@ -24,22 +24,23 @@ pending.change_result(map => { val map1 = - (map /: map.iterator)({ case (m, (file, column)) => - resources.get_model(file) match { - case Some(model) => - val snapshot = model.snapshot() - if (snapshot.is_outdated) m - else { - val html_context = Presentation.html_context() - val document = - Presentation.html_document( - resources, snapshot, html_context, Presentation.elements2) - channel.write(LSP.Preview_Response(file, column, document.title, document.content)) - m - file - } - case None => m - file - } - }) + map.iterator.foldLeft(map) { + case (m, (file, column)) => + resources.get_model(file) match { + case Some(model) => + val snapshot = model.snapshot() + if (snapshot.is_outdated) m + else { + val html_context = Presentation.html_context() + val document = + Presentation.html_document( + resources, snapshot, html_context, Presentation.elements2) + channel.write(LSP.Preview_Response(file, column, document.title, document.content)) + m - file + } + case None => m - file + } + } (map1.nonEmpty, map1) }) } diff -r 78aa7846e91f -r d8a0e996614b src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Thu Mar 04 15:41:46 2021 +0100 @@ -23,7 +23,7 @@ colors: List[Text.Info[Rendering.Color.Value]]): List[VSCode_Model.Decoration] = { val color_ranges = - (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) { + colors.foldLeft(Map.empty[Rendering.Color.Value, List[Text.Range]]) { case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil))) } types.toList.map(c => @@ -324,7 +324,7 @@ Text.Info(entry_range, (entry, model)) <- bibtex_entries_iterator() if entry == name } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range)) - if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _)) + if (iterator.isEmpty) None else Some(iterator.foldLeft(links)(_ :+ _)) case _ => None }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } diff -r 78aa7846e91f -r d8a0e996614b src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Mar 04 15:41:46 2021 +0100 @@ -28,8 +28,8 @@ def update_models(changed: Iterable[(JFile, VSCode_Model)]): State = copy( models = models ++ changed, - pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file }, - pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file }) + pending_input = changed.foldLeft(pending_input) { case (set, (file, _)) => set + file }, + pending_output = changed.foldLeft(pending_output) { case (set, (file, _)) => set + file }) def update_caret(new_caret: Option[(JFile, Line.Position)]): State = if (caret == new_caret) this diff -r 78aa7846e91f -r d8a0e996614b src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 04 15:41:46 2021 +0100 @@ -121,18 +121,19 @@ offset: Text.Offset, documents: List[Document_Structure.Document]): Unit = { - documents.foldLeft(offset) { case (i, document) => - document match { - case Document_Structure.Block(name, text, body) => - val range = Text.Range(i, i + document.length) - val node = - new DefaultMutableTreeNode( - new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range)) - parent.add(node) - make_tree(node, i, body) - case _ => - } - i + document.length + documents.foldLeft(offset) { + case (i, document) => + document match { + case Document_Structure.Block(name, text, body) => + val range = Text.Range(i, i + document.length) + val node = + new DefaultMutableTreeNode( + new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range)) + parent.add(node) + make_tree(node, i, body) + case _ => + } + i + document.length } } diff -r 78aa7846e91f -r d8a0e996614b src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Thu Mar 04 15:41:46 2021 +0100 @@ -267,7 +267,7 @@ val h = painter.getLineHeight * lines + geometry.deco_height val margin1 = if (h <= h_max) { - split_lines(XML.content(formatted)).foldLeft(0.0)({ case (m, line) => m max metric(line) }) + 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 78aa7846e91f -r d8a0e996614b src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/jEdit/src/text_structure.scala Thu Mar 04 15:41:46 2021 +0100 @@ -130,11 +130,12 @@ }).collectFirst({ case (i, true) => i }).getOrElse(0) def indent_brackets: Int = - 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 - else i }) + 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 + else i + } def indent_extra: Int = if (prev_span.exists(keywords.is_quasi_command)) indent_size diff -r 78aa7846e91f -r d8a0e996614b src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Mar 04 15:41:46 2021 +0100 @@ -159,11 +159,12 @@ (node_status.failed, PIDE.options.color_value("error_color")) ).filter(_._1 > 0) - 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 - }) + 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 + } case None => paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) diff -r 78aa7846e91f -r d8a0e996614b src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Mar 04 15:41:46 2021 +0100 @@ -186,9 +186,8 @@ (restriction match { case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name))) case None => snapshot.version.nodes.iterator - }) - .foldLeft(nodes_timing)( - { case (timing1, (name, node)) => + }).foldLeft(nodes_timing) { + case (timing1, (name, node)) => if (PIDE.resources.session_base.loaded_theory(name)) timing1 else { val node_timing = @@ -196,7 +195,7 @@ snapshot.state, snapshot.version, node.commands, threshold = timing_threshold) timing1 + (name -> node_timing) } - }) + } nodes_timing = nodes_timing1 val entries = make_entries()