--- 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))))
+ }
+ }
}
- }
}
}
--- 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"))
}
}
--- 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)
}
}
--- 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 =
--- 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 =
--- 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)
}
--- 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 {
--- 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)
--- 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)
}
--- 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)) }
}
}
--- 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
--- 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
}
}
--- 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) }
}
--- 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) {
--- 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)
--- 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
--- 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 */
--- 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 =
--- 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)
--- 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)
--- 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))
--- 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 =
{
--- 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)
--- 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) =
{
--- 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)
}
--- 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)
--- 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 =
{
--- 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
--- 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))
--- 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))
--- 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)
}
--- 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
--- 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)
--- 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 }
--- 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))
--- 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 */
--- 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)
--- 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)
}
--- 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)
}
--- 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))
}
--- 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)
}
--- 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)
}
--- 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))
--- 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)
--- 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 =
--- 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(
--- 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 */
--- 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
+ }
}
- }
}
}
}
--- 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
--- 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)
}
}
--- 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)
- }
}
}
--- 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
--- 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)
})
}
--- 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 }
--- 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
--- 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
}
}
--- 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
--- 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
--- 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"))
--- 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()