--- 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)
}