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