--- a/src/Pure/Tools/dump.scala Mon Oct 14 19:58:38 2019 +0200
+++ b/src/Pure/Tools/dump.scala Mon Oct 14 20:05:16 2019 +0200
@@ -133,13 +133,7 @@
dirs = session_dirs, strict = true)
}
- def session(logic: String, log: Logger = No_Logger): Session =
- {
- build_logic(logic)
- new Session(context, logic, log, deps.sessions_structure.imports_topological_order)
- }
-
- def partition_sessions(
+ def sessions(
logic: String = default_logic,
log: Logger = No_Logger): List[Session] =
{
@@ -178,7 +172,6 @@
yield new Session(context, logic, log, part)
}
- build_logic(logic)
base ::: List(main) ::: afp
}
}
@@ -324,7 +317,9 @@
Context(options, aspects = aspects, progress = progress, dirs = dirs,
select_dirs = select_dirs, selection = selection)
- context.partition_sessions(logic = logic, log = log).foreach(_.process((args: Args) =>
+ context.build_logic(logic)
+
+ context.sessions(logic = logic, log = log).foreach(_.process((args: Args) =>
{
progress.echo("Processing theory " + args.print_node + " ...")
val aspect_args =
--- a/src/Pure/Tools/update.scala Mon Oct 14 19:58:38 2019 +0200
+++ b/src/Pure/Tools/update.scala Mon Oct 14 20:05:16 2019 +0200
@@ -20,6 +20,8 @@
Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
selection = selection)
+ context.build_logic(logic)
+
val path_cartouches = context.session_options.bool("update_path_cartouches")
def update_xml(xml: XML.Body): XML.Body =
@@ -36,7 +38,7 @@
case t => List(t)
}
- context.session(logic, log = log).process((args: Dump.Args) =>
+ context.sessions(logic, log = log).foreach(_.process((args: Dump.Args) =>
{
progress.echo("Processing theory " + args.print_node + " ...")
@@ -52,7 +54,7 @@
File.write(node_name.path, source1)
}
}
- })
+ }))
}