src/Pure/Tools/update.scala

 
 package isabelle
 
 
 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 */
 
-    context.build_logic(logic)
+    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)
 
-    val path_cartouches = context.options.bool("update_path_cartouches")
+        for (name <- base_logics if !sessions.defined(name)) {
+          error("Base logic " + quote(name) + " outside of session selection")
+        }
+
+        sessions.build_requirements(base_logics).toSet
+      }
+
+
+    /* build */
+
+    val build_results =
+      Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
+        selection = selection)
+
+    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 {
         case XML.Wrapped_Elem(markup, body1, body2) =>
           if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)

           }
         case XML.Elem(_, body) => update_xml(body)
         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
   }
 
 
   /* Isabelle tool wrapper */
 

         var requirements = false
         var exclude_session_groups: List[String] = Nil
         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
 
         val getopts = Getopts("""

     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -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)
     -u OPT       override "update" option: shortcut for "-o update_OPT"
     -v           verbose

         "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
         "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
         "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),
         "u:" -> (arg => options = options + ("update_" + arg)),
         "v" -> (_ => verbose = true),

 
         val sessions = getopts(args)
 
         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)
       })
 }