clarified signature;
authorwenzelm
Mon, 14 Oct 2019 20:05:16 +0200
changeset 71054 e94fec16bf50
parent 71053 d1299774543d
child 71055 4739030a5bf2
clarified signature;
src/Pure/Tools/dump.scala
src/Pure/Tools/update.scala
--- 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)
           }
         }
-      })
+      }))
   }