# HG changeset patch
# User wenzelm
# Date 1567446252 -7200
# Node ID 5f4b8a5050901d2f0720d41414cdfe4e3bf77de4
# Parent  ad7891a7323038d5ba946236c05acc02480aad32
more explicit type Dump.Session, with context information;

diff -r ad7891a73230 -r 5f4b8a505090 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Sep 02 16:28:09 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 02 19:44:12 2019 +0200
@@ -485,18 +485,6 @@
     def options: Options = session_base_info.options
 
 
-    /* dependencies */
-
-    def used_theories(
-      deps: Sessions.Deps, progress: Progress = No_Progress): List[Document.Node.Name] =
-    {
-      for {
-        name <- deps.used_theories_condition(options, progress = progress).topological_order
-        if !session_base.loaded_theory(name.theory)
-      } yield name
-    }
-
-
     /* session */
 
     def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
diff -r ad7891a73230 -r 5f4b8a505090 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Sep 02 16:28:09 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Sep 02 19:44:12 2019 +0200
@@ -13,9 +13,9 @@
 
   sealed case class Aspect_Args(
     options: Options,
+    deps: Sessions.Deps,
     progress: Progress,
     output_dir: Path,
-    deps: Sessions.Deps,
     snapshot: Document.Snapshot,
     status: Document_Status.Node_Status)
   {
@@ -73,135 +73,177 @@
       error("Unknown aspect " + quote(name))
 
 
-  /* dependencies */
-
-  def dependencies(
-    options: Options,
-    progress: Progress = No_Progress,
-    dirs: List[Path] = Nil,
-    select_dirs: List[Path] = Nil,
-    selection: Sessions.Selection = Sessions.Selection.empty): Sessions.Deps =
-  {
-    Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
-      selection_deps(options, selection, progress = progress,
-        uniform_session = true, loading_sessions = true)
-  }
-
-
   /* session */
 
   sealed case class Args(
     session: Headless.Session,
-    deps: Sessions.Deps,
     snapshot: Document.Snapshot,
     status: Document_Status.Node_Status)
   {
     def print_node: String = snapshot.node_name.toString
+  }
 
-    def aspect_args(options: Options, progress: Progress, output_dir: Path): Aspect_Args =
-      Aspect_Args(options, progress, output_dir, deps, snapshot, status)
+  object Session
+  {
+    def apply(
+      options: Options,
+      logic: String,
+      aspects: List[Aspect] = Nil,
+      progress: Progress = No_Progress,
+      log: Logger = No_Logger,
+      dirs: List[Path] = Nil,
+      select_dirs: List[Path] = Nil,
+      selection: Sessions.Selection = Sessions.Selection.empty): Session =
+    {
+      new Session(options, logic, aspects, progress, log, dirs, select_dirs, selection)
+    }
   }
 
-  def session(
-    deps: Sessions.Deps,
-    resources: Headless.Resources,
-    unicode_symbols: Boolean = false,
-    process_theory: Args => Unit,
-    progress: Progress = No_Progress)
+  class Session private(
+    options: Options,
+    logic: String,
+    aspects: List[Aspect],
+    progress: Progress,
+    log: Logger,
+    dirs: List[Path],
+    select_dirs: List[Path],
+    selection: Sessions.Selection)
   {
-    val session = resources.start_session(progress = progress)
-
+    /* context */
 
-    /* asynchronous consumer */
-
-    object Consumer
-    {
-      sealed case class Bad_Theory(
-        name: Document.Node.Name,
-        status: Document_Status.Node_Status,
-        errors: List[String])
-
-      private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory])
+    Build.build_logic(options, logic, build_heap = true, progress = progress,
+      dirs = dirs ::: select_dirs, strict = true)
 
-      private val consumer =
-        Consumer_Thread.fork(name = "dump")(
-          consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
-            {
-              val (snapshot, status) = args
-              val name = snapshot.node_name
-              if (status.ok) {
-                try { process_theory(Args(session, deps, snapshot, status)) }
-                catch {
-                  case exn: Throwable if !Exn.is_interrupt(exn) =>
-                  val msg = Exn.message(exn)
-                  progress.echo("FAILED to process theory " + name)
-                  progress.echo_error_message(msg)
-                  consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
-                }
-              }
-              else {
-                val msgs =
-                  for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
-                  yield {
-                    "Error" + Position.here(pos) + ":\n" +
-                      XML.content(Pretty.formatted(List(tree)))
-                  }
-                progress.echo("FAILED to process theory " + name)
-                msgs.foreach(progress.echo_error_message)
-                consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
-              }
-              true
-            })
+    val dump_options: Options =
+    {
+      val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
+      val options1 =
+        options0 +
+          "completion_limit=0" +
+          "ML_statistics=false" +
+          "parallel_proofs=0" +
+          "editor_tracing_messages=0" +
+          "editor_presentation" +
+          "execution_eager"
+      (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+    }
 
-      def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
-        consumer.send((snapshot, status))
+    val deps: Sessions.Deps =
+      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
+        selection_deps(dump_options, selection, progress = progress,
+          uniform_session = true, loading_sessions = true)
 
-      def shutdown(): List[Bad_Theory] =
-      {
-        consumer.shutdown()
-        consumer_bad_theories.value.reverse
-      }
+    val resources: Headless.Resources =
+      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
+        session_dirs = dirs ::: select_dirs,
+        include_sessions = deps.sessions_structure.imports_topological_order)
+
+    val used_theories: List[Document.Node.Name] =
+    {
+      for {
+        name <- deps.used_theories_condition(dump_options, progress = progress).topological_order
+        if !resources.session_base.loaded_theory(name.theory)
+      } yield name
     }
 
 
-    /* run session */
+    /* run */
+
+    def run(process_theory: Args => Unit, unicode_symbols: Boolean = false)
+    {
+      val session = resources.start_session(progress = progress)
+
+
+      // asynchronous consumer
+
+      object Consumer
+      {
+        sealed case class Bad_Theory(
+          name: Document.Node.Name,
+          status: Document_Status.Node_Status,
+          errors: List[String])
+
+        private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory])
 
-    try {
-      val dump_checkpoint = deps.dump_checkpoint.toSet
-      def commit(snapshot: Document.Snapshot, status: Document_Status.Node_Status)
-      {
-        if (dump_checkpoint(snapshot.node_name)) {
-          session.protocol_command("ML_Heap.share_common_data")
+        private val consumer =
+          Consumer_Thread.fork(name = "dump")(
+            consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
+              {
+                val (snapshot, status) = args
+                val name = snapshot.node_name
+                if (status.ok) {
+                  try { process_theory(Args(session, snapshot, status)) }
+                  catch {
+                    case exn: Throwable if !Exn.is_interrupt(exn) =>
+                    val msg = Exn.message(exn)
+                    progress.echo("FAILED to process theory " + name)
+                    progress.echo_error_message(msg)
+                    consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
+                  }
+                }
+                else {
+                  val msgs =
+                    for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
+                    yield {
+                      "Error" + Position.here(pos) + ":\n" +
+                        XML.content(Pretty.formatted(List(tree)))
+                    }
+                  progress.echo("FAILED to process theory " + name)
+                  msgs.foreach(progress.echo_error_message)
+                  consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
+                }
+                true
+              })
+
+        def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
+          consumer.send((snapshot, status))
+
+        def shutdown(): List[Bad_Theory] =
+        {
+          consumer.shutdown()
+          consumer_bad_theories.value.reverse
         }
-        Consumer.apply(snapshot, status)
       }
 
-      val use_theories = resources.used_theories(deps).map(_.theory)
-      val use_theories_result =
-        session.use_theories(use_theories,
-          unicode_symbols = unicode_symbols,
-          share_common_data = true,
-          progress = progress,
-          commit = Some(commit _))
+
+      // run
 
-      val bad_theories = Consumer.shutdown()
-      val bad_msgs =
-        bad_theories.map(bad =>
-          Output.clean_yxml(
-            "FAILED theory " + bad.name +
-              (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
-              (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", ""))))
-
-      val pending_msgs =
-        use_theories_result.nodes_pending match {
-          case Nil => Nil
-          case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString)))
+      try {
+        val dump_checkpoint = deps.dump_checkpoint.toSet
+        def commit(snapshot: Document.Snapshot, status: Document_Status.Node_Status)
+        {
+          if (dump_checkpoint(snapshot.node_name)) {
+            session.protocol_command("ML_Heap.share_common_data")
+          }
+          Consumer.apply(snapshot, status)
         }
 
-      val errors = bad_msgs ::: pending_msgs
-      if (errors.nonEmpty) error(errors.mkString("\n\n"))
+        val use_theories_result =
+          session.use_theories(used_theories.map(_.theory),
+            unicode_symbols = unicode_symbols,
+            share_common_data = true,
+            progress = progress,
+            commit = Some(commit _))
+
+        val bad_theories = Consumer.shutdown()
+        val bad_msgs =
+          bad_theories.map(bad =>
+            Output.clean_yxml(
+              "FAILED theory " + bad.name +
+                (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
+                (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", ""))))
+
+        val pending_msgs =
+          use_theories_result.nodes_pending match {
+            case Nil => Nil
+            case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString)))
+          }
+
+        val errors = bad_msgs ::: pending_msgs
+        if (errors.nonEmpty) error(errors.mkString("\n\n"))
+      }
+      finally { session.stop() }
     }
-    finally { session.stop() }
   }
 
 
@@ -209,21 +251,9 @@
 
   val default_output_dir: Path = Path.explode("dump")
 
-  def make_options(options: Options, aspects: List[Aspect] = Nil): Options =
-  {
-    val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
-    val options1 =
-      options0 +
-        "completion_limit=0" +
-        "ML_statistics=false" +
-        "parallel_proofs=0" +
-        "editor_tracing_messages=0" +
-        "editor_presentation" +
-        "execution_eager"
-    (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
-  }
-
-  def dump(options: Options, logic: String,
+  def dump(
+    options: Options,
+    logic: String,
     aspects: List[Aspect] = Nil,
     progress: Progress = No_Progress,
     log: Logger = No_Logger,
@@ -232,28 +262,18 @@
     output_dir: Path = default_output_dir,
     selection: Sessions.Selection = Sessions.Selection.empty)
   {
-    Build.build_logic(options, logic, build_heap = true, progress = progress,
-      dirs = dirs ::: select_dirs, strict = true)
-
-    val dump_options = make_options(options, aspects)
-
-    val deps =
-      dependencies(dump_options, progress = progress,
+    val session =
+      Session(options, logic, aspects = aspects, progress = progress, log = log,
         dirs = dirs, select_dirs = select_dirs, selection = selection)
 
-    val resources =
-      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
-        session_dirs = dirs ::: select_dirs,
-        include_sessions = deps.sessions_structure.imports_topological_order)
-
-    session(deps, resources, progress = progress,
-      process_theory = (args: Args) =>
-        {
-          progress.echo("Processing theory " + args.print_node + " ...")
-
-          val aspect_args = args.aspect_args(dump_options, progress, output_dir)
-          aspects.foreach(_.operation(aspect_args))
-        })
+    session.run((args: Args) =>
+      {
+        progress.echo("Processing theory " + args.print_node + " ...")
+        val aspect_args =
+          Aspect_Args(session.dump_options, session.deps, progress, output_dir,
+            args.snapshot, args.status)
+        aspects.foreach(_.operation(aspect_args))
+      })
   }
 
 
diff -r ad7891a73230 -r 5f4b8a505090 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Mon Sep 02 16:28:09 2019 +0200
+++ b/src/Pure/Tools/update.scala	Mon Sep 02 19:44:12 2019 +0200
@@ -16,21 +16,11 @@
     select_dirs: List[Path] = Nil,
     selection: Sessions.Selection = Sessions.Selection.empty)
   {
-    Build.build_logic(options, logic, build_heap = true, progress = progress,
-      dirs = dirs ::: select_dirs, strict = true)
-
-    val dump_options = Dump.make_options(options)
+    val session =
+      Dump.Session(options, logic, progress = progress, log = log, dirs = dirs,
+        select_dirs = select_dirs, selection = selection)
 
-    val deps =
-      Dump.dependencies(dump_options, progress = progress,
-        dirs = dirs, select_dirs = select_dirs, selection = selection)
-
-    val resources =
-      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
-        session_dirs = dirs ::: select_dirs,
-        include_sessions = deps.sessions_structure.imports_topological_order)
-
-    val path_cartouches = dump_options.bool("update_path_cartouches")
+    val path_cartouches = session.dump_options.bool("update_path_cartouches")
 
     def update_xml(xml: XML.Body): XML.Body =
       xml flatMap {
@@ -46,24 +36,23 @@
         case t => List(t)
       }
 
-    Dump.session(deps, resources, progress = progress,
-      process_theory = (args: Dump.Args) =>
-        {
-          progress.echo("Processing theory " + args.print_node + " ...")
+    session.run((args: Dump.Args) =>
+      {
+        progress.echo("Processing theory " + args.print_node + " ...")
 
-          val snapshot = args.snapshot
-          for ((node_name, node) <- snapshot.nodes) {
-            val xml =
-              snapshot.state.markup_to_XML(snapshot.version, node_name,
-                Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
+        val snapshot = args.snapshot
+        for ((node_name, node) <- snapshot.nodes) {
+          val xml =
+            snapshot.state.markup_to_XML(snapshot.version, node_name,
+              Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
 
-            val source1 = Symbol.encode(XML.content(update_xml(xml)))
-            if (source1 != Symbol.encode(node.source)) {
-              progress.echo("Updating " + node_name.path)
-              File.write(node_name.path, source1)
-            }
+          val source1 = Symbol.encode(XML.content(update_xml(xml)))
+          if (source1 != Symbol.encode(node.source)) {
+            progress.echo("Updating " + node_name.path)
+            File.write(node_name.path, source1)
           }
-        })
+        }
+      })
   }