isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
misc tuning and clarification;

--- a/src/Pure/Tools/update.scala	Thu Jan 05 20:13:04 2023 +0100
+++ b/src/Pure/Tools/update.scala	Thu Jan 05 20:25:41 2023 +0100
@@ -8,20 +8,45 @@
 
 
 object Update {
-  def update(options: Options, logic: String,
+  def update(options: Options,
+    base_logics: List[String] = Nil,
     progress: Progress = new Progress,
-    log: Logger = No_Logger,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     selection: Sessions.Selection = Sessions.Selection.empty
-  ): Unit = {
-    val context =
-      Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
-        selection = selection, skip_base = true)
+  ): Build.Results = {
+    /* excluded sessions */
+
+    val exclude: Set[String] =
+      if (base_logics.isEmpty) Set.empty
+      else {
+        val sessions =
+          Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
+            .selection(selection)
+
+        for (name <- base_logics if !sessions.defined(name)) {
+          error("Base logic " + quote(name) + " outside of session selection")
+        }
+
+        sessions.build_requirements(base_logics).toSet
+      }
 
-    context.build_logic(logic)
+
+    /* build */
+
+    val build_results =
+      Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
+        selection = selection)
 
-    val path_cartouches = context.options.bool("update_path_cartouches")
+    if (!build_results.ok) error("Build failed")
+
+    val store = build_results.store
+    val sessions_structure = build_results.deps.sessions_structure
+
+
+    /* update */
+
+    val path_cartouches = options.bool("update_path_cartouches")
 
     def update_xml(xml: XML.Body): XML.Body =
       xml flatMap {
@@ -37,25 +62,40 @@
         case t => List(t)
       }
 
-    context.sessions(logic, log = log).foreach(_.process { (args: Dump.Args) =>
-      progress.echo("Processing theory " + args.print_node + " ...")
+    var seen_theory = Set.empty[String]
 
-      val snapshot = args.snapshot
-      for (node_name <- snapshot.node_files) {
-        val node = snapshot.get_node(node_name)
-        val xml =
-          snapshot.state.xml_markup(snapshot.version, node_name,
-            elements = 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)
+    using(Export.open_database_context(store)) { database_context =>
+      for (session <- sessions_structure.build_topological_order if !exclude(session)) {
+        using(database_context.open_session0(session)) { session_context =>
+          for {
+            db <- session_context.session_db()
+            theory <- store.read_theories(db, session)
+            if !seen_theory(theory)
+          } {
+            seen_theory += theory
+            val theory_context = session_context.theory(theory)
+            for {
+              theory_snapshot <- Build_Job.read_theory(theory_context)
+              node_name <- theory_snapshot.node_files
+              snapshot = theory_snapshot.switch(node_name)
+              if snapshot.node.is_wellformed_text
+            } {
+              progress.expose_interrupt()
+              val source1 =
+                XML.content(update_xml(
+                  snapshot.xml_markup(elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))))
+              if (source1 != snapshot.node.source) {
+                val path = Path.explode(node_name.node)
+                progress.echo("Updating " + quote(File.standard_path(path)))
+                File.write(path, source1)
+              }
+            }
+          }
         }
       }
-    })
+    }
 
-    context.check_errors
+    build_results
   }
 
 
@@ -71,7 +111,7 @@
         var all_sessions = false
         var dirs: List[Path] = Nil
         var session_groups: List[String] = Nil
-        var logic = Dump.default_logic
+        var base_logics: List[String] = Nil
         var options = Options.init()
         var verbose = false
         var exclude_sessions: List[String] = Nil
@@ -85,7 +125,7 @@
     -R           refer to requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
-    -b NAME      base logic image (default """ + isabelle.quote(Dump.default_logic) + """)
+    -b NAME      additional base logic
     -d DIR       include session directory
     -g NAME      select session group NAME
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -100,7 +140,7 @@
         "R" -> (_ => requirements = true),
         "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
         "a" -> (_ => all_sessions = true),
-        "b:" -> (arg => logic = arg),
+        "b:" -> (arg => base_logics ::= arg),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "g:" -> (arg => session_groups = session_groups ::: List(arg)),
         "o:" -> (arg => options = options + arg),
@@ -112,19 +152,23 @@
 
         val progress = new Console_Progress(verbose = verbose)
 
-        progress.interrupt_handler {
-          update(options, logic,
-            progress = progress,
-            dirs = dirs,
-            select_dirs = select_dirs,
-            selection = Sessions.Selection(
-              requirements = requirements,
-              all_sessions = all_sessions,
-              base_sessions = base_sessions,
-              exclude_session_groups = exclude_session_groups,
-              exclude_sessions = exclude_sessions,
-              session_groups = session_groups,
-              sessions = sessions))
-        }
+        val results =
+          progress.interrupt_handler {
+            update(options,
+              base_logics = base_logics,
+              progress = progress,
+              dirs = dirs,
+              select_dirs = select_dirs,
+              selection = Sessions.Selection(
+                requirements = requirements,
+                all_sessions = all_sessions,
+                base_sessions = base_sessions,
+                exclude_session_groups = exclude_session_groups,
+                exclude_sessions = exclude_sessions,
+                session_groups = session_groups,
+                sessions = sessions))
+          }
+
+        sys.exit(results.rc)
       })
 }