diff --git a/etc/options b/etc/options
--- a/etc/options
+++ b/etc/options
@@ -1,370 +1,367 @@
 (* :mode=isabelle-options: *)
 
 section "Document Preparation"
 
 option browser_info : bool = false
   -- "generate theory browser information"
 
 option document : string = ""
   -- "build document in given format: pdf, dvi, false"
 option document_output : string = ""
   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
 option thy_output_break : bool = false
   -- "control line breaks in non-display material"
 option thy_output_cartouche : bool = false
   -- "indicate if the output should be delimited as cartouche"
 option thy_output_quotes : bool = false
   -- "indicate if the output should be delimited via double quotes"
 option thy_output_margin : int = 76
   -- "right margin / page width for printing of display material"
 option thy_output_indent : int = 0
   -- "indentation for pretty printing of display material"
 option thy_output_source : bool = false
   -- "print original source text rather than internal representation"
 option thy_output_source_cartouche : bool = false
   -- "print original source text rather than internal representation, preserve cartouches"
 option thy_output_modes : string = ""
   -- "additional print modes for document output (separated by commas)"
 
 
 section "Prover Output"
 
 option show_types : bool = false
   -- "show type constraints when printing terms"
 option show_sorts : bool = false
   -- "show sort constraints when printing types"
 option show_brackets : bool = false
   -- "show extra brackets when printing terms/types"
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"
 
 option show_consts : bool = false
   -- "show constants with types when printing proof state"
 option show_main_goal : bool = false
   -- "show main goal when printing proof state"
 option goals_limit : int = 10
   -- "maximum number of subgoals to be printed"
 
 option names_long : bool = false
   -- "show fully qualified names"
 option names_short : bool = false
   -- "show base names only"
 option names_unique : bool = true
   -- "show partially qualified names, as required for unique name resolution"
 
 option eta_contract : bool = true
   -- "print terms in eta-contracted form"
 
 option print_mode : string = ""
   -- "additional print modes for prover output (separated by commas)"
 
 
 section "Parallel Processing"
 
 public option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
 option threads_trace : int = 0
   -- "level of tracing information for multithreading"
 option threads_stack_limit : real = 0.25
   -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
 
 public option parallel_limit : int = 0
   -- "approximative limit for parallel tasks (0 = unlimited)"
 public option parallel_print : bool = true
   -- "parallel and asynchronous printing of results"
 public option parallel_proofs : int = 1
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
 
 option command_timing_threshold : real = 0.1
   -- "default threshold for persistent command timing (seconds)"
 
 
 section "Detail of Proof Checking"
 
 option record_proofs : int = -1
   -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false
   -- "skip over proofs (implicit 'sorry')"
 option strict_facts : bool = false
   -- "force lazy facts when defined in context"
 
 
 section "Global Session Parameters"
 
 option condition : string = ""
   -- "required environment variables for subsequent theories (separated by commas)"
 
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
 option timeout_scale : real = 1.0
   -- "scale factor for session timeout"
 
 option process_output_limit : int = 100
   -- "build process output limit (in million characters, 0 = unlimited)"
 
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
 option profiling : string = ""
   -- "ML profiling (possible values: time, allocations)"
 
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
 
 
 section "ML System"
 
 option ML_print_depth : int = 20
   -- "ML print depth for toplevel pretty-printing"
 
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
 public option ML_exception_debugger : bool = false
   -- "ML debugger exception trace for toplevel command execution"
 
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
 public option ML_statistics : bool = true
   -- "ML run-time system statistics"
 
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
 public option ML_process_policy : string = ""
   -- "ML process command prefix (process policy)"
 
 
 section "PIDE Build"
 
 option pide_session : bool = false
   -- "build session heaps via PIDE"
 
-option pide_exports : bool = true
-  -- "store PIDE export artifacts"
-
 option pide_reports : bool = true
   -- "report PIDE markup"
 
 
 section "Editor Session"
 
 public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
 public option editor_input_delay : real = 0.3
   -- "delay for user input (text edits, cursor movement etc.)"
 
 public option editor_generated_input_delay : real = 1.0
   -- "delay for machine-generated input that may outperform user edits"
 
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
 public option editor_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"
 
 option editor_prune_size : int = 0
   -- "retained size of pruned history (delete old versions)"
 
 public option editor_update_delay : real = 0.5
   -- "delay for physical GUI updates"
 
 public option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
 public option editor_tracing_messages : int = 1000
   -- "initial number of tracing messages for each command transaction (0: unbounded)"
 
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
 public option editor_continuous_checking : bool = true
   -- "continuous checking of proof document (visible and required parts)"
 
 public option editor_output_state : bool = false
   -- "implicit output of proof state"
 
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"
 
 option editor_syslog_limit : int = 100
   -- "maximum amount of buffered syslog messages"
 
 public option editor_presentation : bool = false
   -- "dynamic presentation while editing"
 
 
 section "Headless Session"
 
 option headless_consolidate_delay : real = 15
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 option headless_prune_delay : real = 60
   -- "delay to prune history (delete old versions)"
 
 option headless_check_delay : real = 0.5
   -- "delay for theory status check during PIDE processing (seconds)"
 
 option headless_check_limit : int = 0
   -- "maximum number of theory status checks (0 = unlimited)"
 
 option headless_nodes_status_delay : real = -1
   -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)"
 
 option headless_watchdog_timeout : real = 600
   -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)"
 
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
 option headless_load_limit : real = 5.0
   -- "limit in MB for loaded theory files (0 = unlimited)"
 
 
 section "Miscellaneous Tools"
 
 public option find_theorems_limit : int = 40
   -- "limit of displayed results"
 
 public option find_theorems_tactic_limit : int = 5
   -- "limit of tactic search for 'solves' criterion"
 
 
 section "Completion"
 
 public option completion_limit : int = 40
   -- "limit for completion within the formal context"
 
 public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
   -- "glob patterns to ignore in file-system path completion (separated by colons)"
 
 
 section "Spell Checker"
 
 public option spell_checker : bool = true
   -- "enable spell-checker for prose words within document text, comments etc."
 
 public option spell_checker_dictionary : string = "en"
   -- "spell-checker dictionary name"
 
 public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment"
   -- "included markup elements for spell-checker (separated by commas)"
 
 public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text"
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
 section "Secure Shell"
 
 option ssh_config_dir : string = "$HOME/.ssh"
   -- "SSH configuration directory"
 
 option ssh_config_file : string = "$HOME/.ssh/config"
   -- "main SSH configuration file"
 
 option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa"
   -- "possible SSH identity files (separated by colons)"
 
 option ssh_compression : bool = true
   -- "enable SSH compression"
 
 option ssh_connect_timeout : real = 60
   -- "SSH connection timeout (seconds)"
 
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
 
 option ssh_alive_count_max : int = 3
   -- "maximum number of messages to keep SSH server connection alive"
 
 
 section "Phabricator"
 
 option phabricator_version_arcanist : string = "a5bfb968cd90bb0a14c7067e7a2153d5d6ed48d7"
   -- "repository version for arcanist"
 
 option phabricator_version_phabricator : string = "686e51655bb0f4134780dcc68e0276bc9bd0a4af"
   -- "repository version for phabricator"
 
 
 section "Theory Export"
 
 option export_document : bool = false
   -- "export document sources to Isabelle/Scala"
 
 option export_theory : bool = false
   -- "export theory content to Isabelle/Scala"
 
 option export_standard_proofs : bool = false
   -- "export standardized proof terms to Isabelle/Scala (not scalable)"
 
 option export_proofs : bool = false
   -- "export proof terms to Isabelle/Scala"
 
 option prune_proofs : bool = false
   -- "prune proof terms after export (do not store in Isabelle/ML)"
 
 
 section "Theory update"
 
 option update_inner_syntax_cartouches : bool = false
   -- "update inner syntax (types, terms, etc.) to use cartouches"
 
 option update_mixfix_cartouches : bool = false
   -- "update mixfix templates to use cartouches instead of double quotes"
 
 option update_control_cartouches : bool = false
   -- "update antiquotations to use control symbol with cartouche argument"
 
 option update_path_cartouches : bool = false
   -- "update file-system paths to use cartouches"
 
 
 section "Build Database"
 
 option build_database_server : bool = false
 option build_database_user : string = ""
 option build_database_password : string = ""
 option build_database_name : string = ""
 option build_database_host : string = ""
 option build_database_port : int = 0
 option build_database_ssh_host : string = ""
 option build_database_ssh_user : string = ""
 option build_database_ssh_port : int = 0
 
 
 section "Build Log Database"
 
 option build_log_database_user : string = ""
 option build_log_database_password : string = ""
 option build_log_database_name : string = ""
 option build_log_database_host : string = ""
 option build_log_database_port : int = 0
 option build_log_ssh_host : string = ""
 option build_log_ssh_user : string = ""
 option build_log_ssh_port : int = 0
 option build_log_history : int = 30  -- "length of relevant history (in days)"
 option build_log_transaction_size : int = 1  -- "number of log files for each db update"
 
 
 section "Isabelle/Scala/ML system channel"
 
 option system_channel_address : string = ""
 option system_channel_password : string = ""
diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala
+++ b/src/Pure/Admin/build_history.scala
@@ -1,593 +1,596 @@
 /*  Title:      Pure/Admin/build_history.scala
     Author:     Makarius
 
 Build other history versions.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.time.format.DateTimeFormatter
 import java.util.Locale
 
 
 object Build_History
 {
   /* log files */
 
   val engine = "build_history"
   val log_prefix = engine + "_"
 
 
   /* augment settings */
 
   def augment_settings(
     other_isabelle: Other_Isabelle,
     threads: Int,
     arch_64: Boolean,
     heap: Int,
     max_heap: Option[Int],
     more_settings: List[String]): String =
   {
     val (ml_platform, ml_settings) =
     {
       val windows_32 = "x86-windows"
       val windows_64 = "x86_64-windows"
       val windows_64_32 = "x86_64_32-windows"
       val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32")
       val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64")
       val platform_64_32 = platform_64.replace("x86_64-", "x86_64_32-")
 
       val polyml_home =
         try { Path.explode(other_isabelle.getenv("ML_HOME")).dir }
         catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
 
       def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
 
       def err(platform: String): Nothing =
         error("Platform " + platform + " unavailable on this machine")
 
       def check_dir(platform: String): Boolean =
         platform != "" && ml_home(platform).is_dir
 
       val ml_platform =
         if (Platform.is_windows && arch_64) {
           if (check_dir(windows_64)) windows_64 else err(windows_64)
         }
         else if (Platform.is_windows && !arch_64) {
           if (check_dir(windows_64_32)) windows_64_32
           else if (check_dir(windows_32)) windows_32
           else platform_32  // x86-cygwin
         }
         else if (arch_64) {
           if (check_dir(platform_64)) platform_64 else err(platform_64)
         }
         else if (check_dir(platform_64_32)) platform_64_32
         else platform_32
 
       val ml_options =
         "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
         " --gcthreads " + threads +
         (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
 
       (ml_platform,
         List(
           "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
           "ML_PLATFORM=" + quote(ml_platform),
           "ML_OPTIONS=" + quote(ml_options)))
     }
 
     val thread_settings =
       List(
         "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
         "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
 
     val settings =
       List(ml_settings, thread_settings) :::
       (if (more_settings.isEmpty) Nil else List(more_settings))
 
     File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
 
     ml_platform
   }
 
 
 
   /** build_history **/
 
   private val default_user_home = Path.explode("$USER_HOME")
   private val default_rev = "tip"
   private val default_multicore = (1, 1)
   private val default_heap = 1500
   private val default_isabelle_identifier = "build_history"
 
   def build_history(
     options: Options,
     root: Path,
     user_home: Path = default_user_home,
     progress: Progress = new Progress,
     rev: String = default_rev,
     afp_rev: Option[String] = None,
     afp_partition: Int = 0,
     isabelle_identifier: String = default_isabelle_identifier,
     ml_statistics_step: Int = 1,
     components_base: Path = Components.default_components_base,
     fresh: Boolean = false,
     hostname: String = "",
     multicore_base: Boolean = false,
     multicore_list: List[(Int, Int)] = List(default_multicore),
     arch_64: Boolean = false,
     heap: Int = default_heap,
     max_heap: Option[Int] = None,
     init_settings: List[String] = Nil,
     more_settings: List[String] = Nil,
     verbose: Boolean = false,
     build_tags: List[String] = Nil,
     build_args: List[String] = Nil): List[(Process_Result, Path)] =
   {
     /* sanity checks */
 
     if (File.eq(Path.explode("~~"), root))
       error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
 
     for ((threads, _) <- multicore_list if threads < 1)
       error("Bad threads value < 1: " + threads)
     for ((_, processes) <- multicore_list if processes < 1)
       error("Bad processes value < 1: " + processes)
 
     if (heap < 100) error("Bad heap value < 100: " + heap)
 
     if (max_heap.isDefined && max_heap.get < heap)
       error("Bad max_heap value < heap: " + max_heap.get)
 
     System.getenv("ISABELLE_SETTINGS_PRESENT") match {
       case null | "" =>
       case _ => error("Cannot run build_history within existing Isabelle settings environment")
     }
 
 
     /* checkout Isabelle + AFP repository */
 
     def checkout(dir: Path, version: String): String =
     {
       val hg = Mercurial.repository(dir)
       hg.update(rev = version, clean = true)
       progress.echo_if(verbose, hg.log(version, options = "-l1"))
       hg.id(rev = version)
     }
 
     val isabelle_version = checkout(root, rev)
 
     val afp_repos = root + Path.explode("AFP")
     val afp_version = afp_rev.map(checkout(afp_repos, _))
 
     val (afp_build_args, afp_sessions) =
       if (afp_rev.isEmpty) (Nil, Nil)
       else {
         val afp = AFP.init(options, afp_repos)
         (List("-d", "~~/AFP/thys"), afp.partition(afp_partition))
       }
 
 
     /* main */
 
     val other_isabelle =
       Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
         user_home = user_home, progress = progress)
 
     val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
     val build_history_date = Date.now()
     val build_group_id = build_host + ":" + build_history_date.time.ms
 
     var first_build = true
     for ((threads, processes) <- multicore_list) yield
     {
       /* init settings */
 
       val component_settings =
         other_isabelle.init_components(
           components_base = components_base, catalogs = List("main", "optional"))
       other_isabelle.init_settings(component_settings ::: init_settings)
       other_isabelle.resolve_components(verbose)
       val ml_platform =
         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
 
       val isabelle_output =
         other_isabelle.isabelle_home_user + Path.explode("heaps") +
           Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
       val isabelle_output_log = isabelle_output + Path.explode("log")
       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
 
       if (first_build) {
         other_isabelle.resolve_components(verbose)
 
         if (fresh)
           Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
         other_isabelle.bash(
           "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
             "bin/isabelle jedit -b", redirect = true, echo = verbose).check
 
         for {
           tool <- List("ghc_setup", "ocaml_setup")
           if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" &&
             (other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file
         } other_isabelle(tool, echo = verbose)
 
         Isabelle_System.rm_tree(isabelle_base_log)
       }
 
       Isabelle_System.rm_tree(isabelle_output)
       Isabelle_System.mkdirs(isabelle_output)
 
       val log_path =
         other_isabelle.isabelle_home_user +
           Build_Log.log_subdir(build_history_date) +
           Build_Log.log_filename(Build_History.engine, build_history_date,
             List(build_host, ml_platform, "M" + threads) ::: build_tags)
 
       Isabelle_System.mkdirs(log_path.dir)
 
       val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
       val build_out_progress = new File_Progress(build_out)
       build_out.file.delete
 
 
       /* build */
 
       if (multicore_base && !first_build && isabelle_base_log.is_dir)
         Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
 
       val build_start = Date.now()
       val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
-      val build_result =
+
+      val build_isabelle =
         Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
-          user_home = user_home, progress = build_out_progress)(
-            "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true,
-            strict = false)
+          user_home = user_home, progress = build_out_progress)
+      val build_result =
+        build_isabelle("build " + Bash.strings(build_args1 ::: afp_sessions),
+          redirect = true, echo = true, strict = false)
+
       val build_end = Date.now()
 
       val build_info: Build_Log.Build_Info =
         Build_Log.Log_File(log_path.file_name, build_result.out_lines).
           parse_build_info(ml_statistics = true)
 
 
       /* output log */
 
       val store = Sessions.store(options + "build_database_server=false")
 
       val meta_info =
         Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
         Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
         List(
           Build_Log.Prop.build_group_id.name -> build_group_id,
           Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),
           Build_Log.Prop.build_engine.name -> Build_History.engine,
           Build_Log.Prop.build_host.name -> build_host,
           Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start),
           Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end),
           Build_Log.Prop.isabelle_version.name -> isabelle_version) :::
         afp_version.map(Build_Log.Prop.afp_version.name -> _).toList
 
       build_out_progress.echo("Reading session build info ...")
       val session_build_info =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
 
             if (database.is_file) {
               using(SQLite.open_database(database))(db =>
               {
                 val theory_timings =
                   try {
                     store.read_theory_timings(db, session_name).map(ps =>
                       Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
                   }
                   catch { case ERROR(_) => Nil }
 
                 val session_sources =
                   store.read_build(db, session_name).map(_.sources) match {
                     case Some(sources) if sources.length == SHA1.digest_length =>
                       List("Sources " + session_name + " " + sources)
                     case _ => Nil
                   }
 
                 theory_timings ::: session_sources
               })
             }
             else Nil
           })
 
       build_out_progress.echo("Reading ML statistics ...")
       val ml_statistics =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
             val log_gz = isabelle_output + store.log_gz(session_name)
 
             val properties =
               if (database.is_file) {
                 using(SQLite.open_database(database))(db =>
                   store.read_ml_statistics(db, session_name))
               }
               else if (log_gz.is_file) {
                 Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
               }
               else Nil
 
             val trimmed_properties =
               if (ml_statistics_step <= 0) Nil
               else if (ml_statistics_step == 1) properties
               else {
                 (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
                  yield ps).toList
               }
 
             trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
           })
 
       build_out_progress.echo("Reading error messages ...")
       val session_errors =
         build_info.failed_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
             val errors =
               if (database.is_file) {
                 try {
                   using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
                 } // column "errors" could be missing
                 catch { case _: java.sql.SQLException => Nil }
               }
               else Nil
             errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
           })
 
       build_out_progress.echo("Reading heap sizes ...")
       val heap_sizes =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val heap = isabelle_output + Path.explode(session_name)
             if (heap.is_file)
               Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
             else None
           })
 
       build_out_progress.echo("Writing log file " + log_path.ext("xz") + " ...")
       File.write_xz(log_path.ext("xz"),
         terminate_lines(
           Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines :::
           session_build_info :::
           ml_statistics.map(Protocol.ML_Statistics_Marker.apply) :::
           session_errors.map(Protocol.Error_Message_Marker.apply) :::
           heap_sizes), XZ.options(6))
 
 
       /* next build */
 
       if (multicore_base && first_build && isabelle_output_log.is_dir)
         Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
 
       Isabelle_System.rm_tree(isabelle_output)
 
       first_build = false
 
       (build_result, log_path.ext("xz"))
     }
   }
 
 
   /* command line entry point */
 
   private object Multicore
   {
     private val Pat1 = """^(\d+)$""".r
     private val Pat2 = """^(\d+)x(\d+)$""".r
 
     def parse(s: String): (Int, Int) =
       s match {
         case Pat1(Value.Int(x)) => (x, 1)
         case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
         case _ => error("Bad multicore configuration: " + quote(s))
       }
   }
 
   def main(args: Array[String])
   {
     Command_Line.tool {
       var afp_rev: Option[String] = None
       var multicore_base = false
       var components_base: Path = Components.default_components_base
       var heap: Option[Int] = None
       var max_heap: Option[Int] = None
       var multicore_list = List(default_multicore)
       var isabelle_identifier = default_isabelle_identifier
       var afp_partition = 0
       var more_settings: List[String] = Nil
       var fresh = false
       var hostname = ""
       var init_settings: List[String] = Nil
       var arch_64 = false
       var output_file = ""
       var rev = default_rev
       var ml_statistics_step = 1
       var build_tags = List.empty[String]
       var user_home = default_user_home
       var verbose = false
       var exit_code = false
 
       val getopts = Getopts("""
 Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...]
 
   Options are:
     -A REV       include $ISABELLE_HOME/AFP repository at given revision
     -B           first multicore build serves as base for scheduling information
     -C DIR       base directory for Isabelle components (default: """ +
       Components.default_components_base + """)
     -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
       default_heap * 2 + """ for x86_64)
     -M MULTICORE multicore configurations (see below)
     -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
     -P NUMBER    AFP partition number (0, 1, 2, default: 0=unrestricted)
     -U SIZE      maximal ML heap in MB (default: unbounded)
     -e TEXT      additional text for generated etc/settings
     -f           fresh build of Isabelle/Scala components (recommended)
     -h NAME      override local hostname
     -i TEXT      initial text for generated etc/settings
     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
     -o FILE      output file for log names (default: stdout)
     -r REV       update to revision (default: """ + default_rev + """)
     -s NUMBER    step size for ML statistics (0=none, 1=all, n=step, default: 1)
     -t TAG       free-form build tag (multiple occurrences possible)
     -u DIR       alternative USER_HOME directory
     -v           verbose
     -x           return overall exit code from build processes
 
   Build Isabelle sessions from the history of another REPOSITORY clone,
   passing ARGS directly to its isabelle build tool.
 
   Each MULTICORE configuration consists of one or two numbers (default 1):
   THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
 """,
         "A:" -> (arg => afp_rev = Some(arg)),
         "B" -> (_ => multicore_base = true),
         "C:" -> (arg => components_base = Path.explode(arg)),
         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
         "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
         "N:" -> (arg => isabelle_identifier = arg),
         "P:" -> (arg => afp_partition = Value.Int.parse(arg)),
         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
         "e:" -> (arg => more_settings = more_settings ::: List(arg)),
         "f" -> (_ => fresh = true),
         "h:" -> (arg => hostname = arg),
         "i:" -> (arg => init_settings = init_settings ::: List(arg)),
         "m:" ->
           {
             case "32" | "x86" => arch_64 = false
             case "64" | "x86_64" => arch_64 = true
             case bad => error("Bad processor architecture: " + quote(bad))
           },
         "o:" -> (arg => output_file = arg),
         "r:" -> (arg => rev = arg),
         "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
         "t:" -> (arg => build_tags = build_tags ::: List(arg)),
         "u:" -> (arg => user_home = Path.explode(arg)),
         "v" -> (_ => verbose = true),
         "x" -> (_ => exit_code = true))
 
       val more_args = getopts(args)
       val (root, build_args) =
         more_args match {
           case root :: build_args => (Path.explode(root), build_args)
           case _ => getopts.usage()
         }
 
       val progress = new Console_Progress(stderr = true)
 
       val results =
         build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
           afp_rev = afp_rev, afp_partition = afp_partition,
           isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
           components_base = components_base, fresh = fresh, hostname = hostname,
           multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
           max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
           verbose = verbose, build_tags = build_tags, build_args = build_args)
 
       if (output_file == "") {
         for ((_, log_path) <- results)
           Output.writeln(log_path.implode, stdout = true)
       }
       else {
         File.write(Path.explode(output_file),
           cat_lines(for ((_, log_path) <- results) yield log_path.implode))
       }
 
       val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
       if (rc != 0 && exit_code) sys.exit(rc)
     }
   }
 
 
 
   /** remote build_history -- via command-line **/
 
   def remote_build_history(
     ssh: SSH.Session,
     isabelle_repos_self: Path,
     isabelle_repos_other: Path,
     isabelle_repos_source: String = Isabelle_Cronjob.isabelle_repos_source,
     afp_repos_source: String = AFP.repos_source,
     isabelle_identifier: String = "remote_build_history",
     self_update: Boolean = false,
     progress: Progress = new Progress,
     rev: String = "",
     afp_rev: Option[String] = None,
     options: String = "",
     args: String = ""): List[(String, Bytes)] =
   {
     /* Isabelle self repository */
 
     val self_hg =
       Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
 
     def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
       ssh.execute(
         Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
           ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args,
         progress_stdout = progress.echo_if(echo, _),
         progress_stderr = progress.echo_if(echo, _),
         strict = strict).check
 
     if (self_update) {
       val hg = Mercurial.repository(Path.explode("~~"))
       hg.push(self_hg.root_url, force = true)
       self_hg.update(rev = hg.parent(), clean = true)
 
       execute("bin/isabelle", "components -I")
       execute("bin/isabelle", "components -a", echo = true)
       execute("Admin/build", "jars_fresh")
     }
 
     val rev_id = self_hg.id(rev)
 
 
     /* Isabelle other + AFP repository */
 
     if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
       ssh.rm_tree(isabelle_repos_other)
     }
     val other_hg =
       Mercurial.clone_repository(
         ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh)
 
     val afp_options =
       if (afp_rev.isEmpty) ""
       else {
         val afp_repos = isabelle_repos_other + Path.explode("AFP")
         val afp_hg = Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh)
         " -A " + Bash.string(afp_rev.get)
       }
 
 
     /* Admin/build_history */
 
     ssh.with_tmp_dir(tmp_dir =>
     {
       val output_file = tmp_dir + Path.explode("output")
 
       execute("Admin/build_history",
         "-o " + ssh.bash_path(output_file) +
           (if (rev == "") "" else " -r " + Bash.string(rev_id)) + " " +
           options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args,
         echo = true, strict = false)
 
       for (line <- split_lines(ssh.read(output_file)))
       yield {
         val log = Path.explode(line)
         val bytes = ssh.read_bytes(log)
         ssh.rm(log)
         (log.file_name, bytes)
       }
     })
   }
 }
diff --git a/src/Pure/PIDE/protocol_handlers.scala b/src/Pure/PIDE/protocol_handlers.scala
--- a/src/Pure/PIDE/protocol_handlers.scala
+++ b/src/Pure/PIDE/protocol_handlers.scala
@@ -1,95 +1,95 @@
 /*  Title:      Pure/PIDE/protocol_handlers.scala
     Author:     Makarius
 
 Management of add-on protocol handlers for PIDE session.
 */
 
 package isabelle
 
 
 object Protocol_Handlers
 {
   private def bad_handler(exn: Throwable, name: String): Unit =
     Output.error_message(
       "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
 
   sealed case class State(
     session: Session,
     handlers: Map[String, Session.Protocol_Handler] = Map.empty,
-    functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
+    functions: Map[String, Session.Protocol_Function] = Map.empty)
   {
     def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
 
     def init(handler: Session.Protocol_Handler): State =
     {
       val name = handler.getClass.getName
 
       val (handlers1, functions1) =
         handlers.get(name) match {
           case Some(old_handler) =>
             Output.warning("Redefining protocol handler: " + name)
             old_handler.exit()
             (handlers - name, functions -- old_handler.functions.map(_._1))
           case None => (handlers, functions)
         }
 
       val (handlers2, functions2) =
         try {
           handler.init(session)
 
           val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
           if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
 
           (handlers1 + (name -> handler), functions1 ++ handler.functions)
         }
         catch {
           case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
         }
       copy(handlers = handlers2, functions = functions2)
     }
 
     def init(name: String): State =
     {
       val new_handler =
         try {
           Some(Class.forName(name).getDeclaredConstructor().newInstance()
             .asInstanceOf[Session.Protocol_Handler])
         }
         catch { case exn: Throwable => bad_handler(exn, name); None }
       new_handler match { case Some(handler) => init(handler) case None => this }
     }
 
     def invoke(msg: Prover.Protocol_Output): Boolean =
       msg.properties match {
         case (Markup.FUNCTION, a) :: _ if functions.isDefinedAt(a) =>
           try { functions(a)(msg) }
           catch {
             case exn: Throwable =>
               Output.error_message(
                 "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
             false
           }
         case _ => false
       }
 
     def exit(): State =
     {
       for ((_, handler) <- handlers) handler.exit()
       copy(handlers = Map.empty, functions = Map.empty)
     }
   }
 
   def init(session: Session): Protocol_Handlers =
     new Protocol_Handlers(session)
 }
 
 class Protocol_Handlers private(session: Session)
 {
   private val state = Synchronized(Protocol_Handlers.State(session))
 
   def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
   def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
   def init(name: String): Unit = state.change(_.init(name))
   def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
   def exit(): Unit = state.change(_.exit())
 }
diff --git a/src/Pure/PIDE/prover.scala b/src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala
+++ b/src/Pure/PIDE/prover.scala
@@ -1,368 +1,368 @@
 /*  Title:      Pure/PIDE/prover.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Prover process wrapping.
 */
 
 package isabelle
 
 
 import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
 
 
 object Prover
 {
   /* messages */
 
   sealed abstract class Message
   type Receiver = Message => Unit
 
   class Input(val name: String, val args: List[String]) extends Message
   {
     override def toString: String =
       XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
         args.flatMap(s =>
           List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString
   }
 
   class Output(val message: XML.Elem) extends Message
   {
     def kind: String = message.markup.name
     def properties: Properties.T = message.markup.properties
     def body: XML.Body = message.body
 
     def is_init: Boolean = kind == Markup.INIT
     def is_exit: Boolean = kind == Markup.EXIT
     def is_stdout: Boolean = kind == Markup.STDOUT
     def is_stderr: Boolean = kind == Markup.STDERR
     def is_system: Boolean = kind == Markup.SYSTEM
     def is_status: Boolean = kind == Markup.STATUS
     def is_report: Boolean = kind == Markup.REPORT
     def is_syslog: Boolean = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
       val res =
         if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body, metric = Symbol.Metric)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
       else
         kind.toString + " " +
           (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
     }
   }
 
   class Protocol_Output(props: Properties.T, val bytes: Bytes)
     extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
   {
     lazy val text: String = bytes.text
   }
 }
 
 
 class Prover(
   receiver: Prover.Receiver,
   xml_cache: XML.Cache,
   channel: System_Channel,
   process: Bash.Process) extends Protocol
 {
   /** receiver output **/
 
   private def system_output(text: String)
   {
     receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
   private def protocol_output(props: Properties.T, bytes: Bytes)
   {
-    receiver(new Prover.Protocol_Output(props, bytes))
+    receiver(new Prover.Protocol_Output(xml_cache.props(props), bytes))
   }
 
   private def output(kind: String, props: Properties.T, body: XML.Body)
   {
     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
     val reports = Protocol_Message.reports(props, body)
     for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
   }
 
   private def exit_message(result: Process_Result)
   {
     output(Markup.EXIT, Markup.Process_Result(result),
       List(XML.Text(result.print_return_code)))
   }
 
 
 
   /** process manager **/
 
   private val process_result: Future[Process_Result] =
     Future.thread("process_result") {
       val rc = process.join
       val timing = process.get_timing
       Process_Result(rc, timing = timing)
     }
 
   private def terminate_process()
   {
     try { process.terminate }
     catch {
       case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
     }
   }
 
   private val process_manager = Isabelle_Thread.fork(name = "process_manager")
   {
     val stdout = physical_output(false)
 
     val (startup_failed, startup_errors) =
     {
       var finished: Option[Boolean] = None
       val result = new StringBuilder(100)
       while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
         while (finished.isEmpty && process.stderr.ready) {
           try {
             val c = process.stderr.read
             if (c == 2) finished = Some(true)
             else result += c.toChar
           }
           catch { case _: IOException => finished = Some(false) }
         }
         Time.seconds(0.05).sleep
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
     if (startup_errors != "") system_output(startup_errors)
 
     if (startup_failed) {
       terminate_process()
       process_result.join
       stdout.join
       exit_message(Process_Result(127))
     }
     else {
       val (command_stream, message_stream) = channel.rendezvous()
 
       command_input_init(command_stream)
       val stderr = physical_output(true)
       val message = message_output(message_stream)
 
       val result = process_result.join
       system_output("process terminated")
       command_input_close()
       for (thread <- List(stdout, stderr, message)) thread.join
       system_output("process_manager terminated")
       exit_message(result)
     }
     channel.shutdown()
   }
 
 
   /* management methods */
 
   def join() { process_manager.join() }
 
   def terminate()
   {
     system_output("Terminating prover process")
     command_input_close()
 
     var count = 10
     while (!process_result.is_finished && count > 0) {
       Time.seconds(0.1).sleep
       count -= 1
     }
     if (!process_result.is_finished) terminate_process()
   }
 
 
 
   /** process streams **/
 
   /* command input */
 
   private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
 
   private def command_input_close(): Unit = command_input.foreach(_.shutdown)
 
   private def command_input_init(raw_stream: OutputStream)
   {
     val name = "command_input"
     val stream = new BufferedOutputStream(raw_stream)
     command_input =
       Some(
         Consumer_Thread.fork(name)(
           consume =
             {
               case chunks =>
                 try {
                   Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream)
                   chunks.foreach(_.write_stream(stream))
                   stream.flush
                   true
                 }
                 catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
             },
           finish = { case () => stream.close; system_output(name + " terminated") }
         )
       )
   }
 
 
   /* physical output */
 
   private def physical_output(err: Boolean): Thread =
   {
     val (name, reader, markup) =
       if (err) ("standard_error", process.stderr, Markup.STDERR)
       else ("standard_output", process.stdout, Markup.STDOUT)
 
     Isabelle_Thread.fork(name = name) {
       try {
         var result = new StringBuilder(100)
         var finished = false
         while (!finished) {
           //{{{
           var c = -1
           var done = false
           while (!done && (result.isEmpty || reader.ready)) {
             c = reader.read
             if (c >= 0) result.append(c.asInstanceOf[Char])
             else done = true
           }
           if (result.nonEmpty) {
             output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
             result.clear
           }
           else {
             reader.close
             finished = true
           }
           //}}}
         }
       }
       catch { case e: IOException => system_output(name + ": " + e.getMessage) }
       system_output(name + " terminated")
     }
   }
 
 
   /* message output */
 
   private def message_output(stream: InputStream): Thread =
   {
     class EOF extends Exception
     class Protocol_Error(msg: String) extends Exception(msg)
 
     val name = "message_output"
     Isabelle_Thread.fork(name = name) {
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
       def read_int(): Int =
       //{{{
       {
         var n = 0
         c = stream.read
         if (c == -1) throw new EOF
         while (48 <= c && c <= 57) {
           n = 10 * n + (c - 48)
           c = stream.read
         }
         if (c != 10)
           throw new Protocol_Error("malformed header: expected integer followed by newline")
         else n
       }
       //}}}
 
       def read_chunk_bytes(): (Array[Byte], Int) =
       //{{{
       {
         val n = read_int()
         val buf =
           if (n <= default_buffer.length) default_buffer
           else new Array[Byte](n)
 
         var i = 0
         var m = 0
         do {
           m = stream.read(buf, i, n - i)
           if (m != -1) i += m
         }
         while (m != -1 && n > i)
 
         if (i != n)
           throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
 
         (buf, n)
       }
       //}}}
 
       def read_chunk(): XML.Body =
       {
         val (buf, n) = read_chunk_bytes()
         YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n))
       }
 
       try {
         do {
           try {
             val header = read_chunk()
             header match {
               case List(XML.Elem(Markup(name, props), Nil)) =>
                 val kind = name.intern
                 if (kind == Markup.PROTOCOL) {
                   val (buf, n) = read_chunk_bytes()
                   protocol_output(props, Bytes(buf, 0, n))
                 }
                 else {
                   val body = read_chunk()
                   output(kind, props, body)
                 }
               case _ =>
                 read_chunk()
                 throw new Protocol_Error("bad header: " + header.toString)
             }
           }
           catch { case _: EOF => }
         }
         while (c != -1)
       }
       catch {
         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
         case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
       }
       stream.close
 
       system_output(name + " terminated")
     }
   }
 
 
 
   /** protocol commands **/
 
   var trace: Boolean = false
 
   def protocol_command_raw(name: String, args: List[Bytes]): Unit =
     command_input match {
       case Some(thread) if thread.is_active =>
         if (trace) {
           val payload = (0 /: args)({ case (n, b) => n + b.length })
           Output.writeln(
             "protocol_command " + name + ", args = " + args.length + ", payload = " + payload)
         }
         thread.send(Bytes(name) :: args)
       case _ => error("Inactive prover input thread for command " + quote(name))
     }
 
   def protocol_command_args(name: String, args: List[String])
   {
     receiver(new Prover.Input(name, args))
     protocol_command_raw(name, args.map(Bytes(_)))
   }
 
   def protocol_command(name: String, args: String*): Unit =
     protocol_command_args(name, args.toList)
 }
diff --git a/src/Pure/PIDE/session.scala b/src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala
+++ b/src/Pure/PIDE/session.scala
@@ -1,750 +1,750 @@
 /*  Title:      Pure/PIDE/session.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 PIDE editor session, potentially with running prover process.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.Queue
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 
 object Session
 {
   /* outlets */
 
   object Consumer
   {
     def apply[A](name: String)(consume: A => Unit): Consumer[A] =
       new Consumer[A](name, consume)
   }
   final class Consumer[-A] private(val name: String, val consume: A => Unit)
 
   class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
   {
     private val consumers = Synchronized[List[Consumer[A]]](Nil)
 
     def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
     def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
 
     def post(a: A)
     {
       for (c <- consumers.value.iterator) {
         dispatcher.send(() =>
           try { c.consume(a) }
           catch {
             case exn: Throwable =>
               Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
           })
       }
     }
   }
 
 
   /* change */
 
   sealed case class Change(
     previous: Document.Version,
     syntax_changed: List[Document.Node.Name],
     deps_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
     consolidate: List[Document.Node.Name],
     version: Document.Version)
 
   case object Change_Flush
 
 
   /* events */
 
   //{{{
   case class Command_Timing(props: Properties.T)
   case class Theory_Timing(props: Properties.T)
   case class Runtime_Statistics(props: Properties.T)
   case class Task_Statistics(props: Properties.T)
   case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
   case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
   sealed abstract class Phase
   {
     def print: String =
       this match {
         case Terminated(result) => if (result.ok) "finished" else "failed"
         case _ => Word.lowercase(this.toString)
       }
   }
   case object Inactive extends Phase  // stable
   case object Startup extends Phase  // transient
   case object Ready extends Phase  // metastable
   case object Shutdown extends Phase  // transient
   case class Terminated(result: Process_Result) extends Phase  // stable
   //}}}
 
 
   /* syslog */
 
   private[Session] class Syslog(limit: Int)
   {
     private var queue = Queue.empty[XML.Elem]
     private var length = 0
 
     def += (msg: XML.Elem): Unit = synchronized {
       queue = queue.enqueue(msg)
       length += 1
       if (length > limit) queue = queue.dequeue._2
     }
 
     def content: String = synchronized {
       cat_lines(queue.iterator.map(XML.content)) +
       (if (length > limit) "\n(A total of " + length + " messages...)" else "")
     }
   }
 
 
   /* protocol handlers */
 
+  type Protocol_Function = Prover.Protocol_Output => Boolean
+
   abstract class Protocol_Handler
   {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
-    val functions: List[(String, Prover.Protocol_Output => Boolean)]
+    val functions: List[(String, Protocol_Function)]
   }
 }
 
 
 class Session(_session_options: => Options, val resources: Resources) extends Document.Session
 {
   session =>
 
   val xml_cache: XML.Cache = XML.make_cache()
   val xz_cache: XZ.Cache = XZ.make_cache()
 
 
   /* global flags */
 
   @volatile var timing: Boolean = false
   @volatile var verbose: Boolean = false
 
 
   /* dynamic session options */
 
   def session_options: Options = _session_options
 
   def output_delay: Time = session_options.seconds("editor_output_delay")
   def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay")
   def prune_delay: Time = session_options.seconds("editor_prune_delay")
   def prune_size: Int = session_options.int("editor_prune_size")
   def syslog_limit: Int = session_options.int("editor_syslog_limit")
   def reparse_limit: Int = session_options.int("editor_reparse_limit")
 
 
   /* dispatcher */
 
   private val dispatcher =
     Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
 
   def assert_dispatcher[A](body: => A): A =
   {
     assert(dispatcher.check_thread)
     body
   }
 
   def require_dispatcher[A](body: => A): A =
   {
     require(dispatcher.check_thread)
     body
   }
 
   def send_dispatcher(body: => Unit): Unit =
   {
     if (dispatcher.check_thread) body
     else dispatcher.send(() => body)
   }
 
   def send_wait_dispatcher(body: => Unit): Unit =
   {
     if (dispatcher.check_thread) body
     else dispatcher.send_wait(() => body)
   }
 
 
   /* outlets */
 
   val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher)
   val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher)
   val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher)
   val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher)
   val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
   val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
   val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher)
   val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher)
   val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
   val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
   val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
   val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
   val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher)
 
   val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck!
 
 
   /** main protocol manager **/
 
   /* internal messages */
 
   private case class Start(start_prover: Prover.Receiver => Prover)
   private case object Stop
   private case class Get_State(promise: Promise[Document.State])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Update_Options(options: Options)
   private case object Consolidate_Execution
   private case object Prune_History
 
 
   /* phase */
 
   private def post_phase(new_phase: Session.Phase): Session.Phase =
   {
     phase_changed.post(new_phase)
     new_phase
   }
   private val _phase = Synchronized[Session.Phase](Session.Inactive)
   private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase))
 
   def phase: Session.Phase = _phase.value
   def is_ready: Boolean = phase == Session.Ready
 
 
   /* syslog */
 
   private val syslog = new Session.Syslog(syslog_limit)
   def syslog_content(): String = syslog.content
 
 
   /* pipelined change parsing */
 
   private case class Text_Edits(
     previous: Future[Document.Version],
     doc_blobs: Document.Blobs,
     text_edits: List[Document.Edit_Text],
     consolidate: List[Document.Node.Name],
     version_result: Promise[Document.Version])
 
   private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
   {
     case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
       val prev = previous.get_finished
       val change =
         Timing.timeit("parse_change", timing) {
           resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
         }
       version_result.fulfill(change.version)
       manager.send(change)
       true
   }
 
 
   /* buffered changes */
 
   private object change_buffer
   {
     private var assignment: Boolean = false
     private var nodes: Set[Document.Node.Name] = Set.empty
     private var commands: Set[Command] = Set.empty
 
     def flush(): Unit = synchronized {
       if (assignment || nodes.nonEmpty || commands.nonEmpty)
         commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
       if (nodes.nonEmpty) consolidation.update(nodes)
       assignment = false
       nodes = Set.empty
       commands = Set.empty
     }
     private val delay_flush = Delay.first(output_delay) { flush() }
 
     def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
       synchronized {
         assignment |= assign
         for (node <- edited_nodes) {
           nodes += node
         }
         for (command <- cmds) {
           nodes += command.node_name
           command.blobs_names.foreach(nodes += _)
           commands += command
         }
         delay_flush.invoke()
       }
 
     def shutdown()
     {
       delay_flush.revoke()
       flush()
     }
   }
 
 
   /* postponed changes */
 
   private object postponed_changes
   {
     private var postponed: List[Session.Change] = Nil
 
     def store(change: Session.Change): Unit = synchronized { postponed ::= change }
 
     def flush(state: Document.State): List[Session.Change] = synchronized {
       val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
       postponed = unassigned
       assigned.reverse
     }
   }
 
 
   /* node consolidation */
 
   private object consolidation
   {
     private val delay =
       Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) }
 
     private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
     private val state = Synchronized(init_state)
 
     def exit()
     {
       delay.revoke()
       state.change(_ => None)
     }
 
     def update(new_nodes: Set[Document.Node.Name] = Set.empty)
     {
       val active =
         state.change_result(st =>
           (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)))
       if (active) delay.invoke()
     }
 
     def flush(): Set[Document.Node.Name] =
       state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None))
   }
 
 
   /* prover process */
 
   private object prover
   {
     private val variable = Synchronized[Option[Prover]](None)
 
     def defined: Boolean = variable.value.isDefined
     def get: Prover = variable.value.get
     def set(p: Prover) { variable.change(_ => Some(p)) }
     def reset { variable.change(_ => None) }
     def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) }
   }
 
 
   /* file formats */
 
   lazy val file_formats: File_Format.Session =
     File_Format.registry.start_session(session)
 
 
   /* protocol handlers */
 
   private val protocol_handlers = Protocol_Handlers.init(session)
 
   def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
     protocol_handlers.get(name)
 
   def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
     protocol_handlers.init(handler)
 
   def init_protocol_handler(name: String): Unit =
     protocol_handlers.init(name)
 
 
   /* debugger */
 
   private val debugger_handler = new Debugger.Handler(this)
   init_protocol_handler(debugger_handler)
 
   def debugger: Debugger = debugger_handler.debugger
 
 
   /* manager thread */
 
   private val delay_prune =
     Delay.first(prune_delay) { manager.send(Prune_History) }
 
   private val manager: Consumer_Thread[Any] =
   {
     /* global state */
     val global_state = Synchronized(Document.State.init)
 
 
     /* raw edits */
 
     def handle_raw_edits(
       doc_blobs: Document.Blobs = Document.Blobs.empty,
       edits: List[Document.Edit_Text] = Nil,
       consolidate: List[Document.Node.Name] = Nil)
     //{{{
     {
       require(prover.defined)
 
       if (edits.nonEmpty) prover.get.discontinue_execution()
 
       val previous = global_state.value.history.tip.version
       val version = Future.promise[Document.Version]
       global_state.change(_.continue_history(previous, edits, version))
 
       raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
       change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version))
     }
     //}}}
 
 
     /* resulting changes */
 
     def handle_change(change: Session.Change)
     //{{{
     {
       require(prover.defined)
 
       // define commands
       {
         val id_commands = new mutable.ListBuffer[Command]
         def id_command(command: Command)
         {
           for {
             (name, digest) <- command.blobs_defined
             if !global_state.value.defined_blob(digest)
           } {
             change.version.nodes(name).get_blob match {
               case Some(blob) =>
                 global_state.change(_.define_blob(digest))
                 prover.get.define_blob(digest, blob.bytes)
               case None =>
                 Output.error_message("Missing blob " + quote(name.toString))
             }
           }
 
           if (!global_state.value.defined_command(command.id)) {
             global_state.change(_.define_command(command))
             id_commands += command
           }
         }
         for { (_, edit) <- change.doc_edits } {
           edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) })
         }
         if (id_commands.nonEmpty) prover.get.define_commands_bulk(id_commands.toList)
       }
 
       val assignment = global_state.value.the_assignment(change.previous).check_finished
       global_state.change(_.define_version(change.version, assignment))
 
       prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
       resources.commit(change)
     }
     //}}}
 
 
     /* prover output */
 
     def handle_output(output: Prover.Output)
     //{{{
     {
       def bad_output()
       {
         if (verbose)
           Output.warning("Ignoring bad prover output: " + output.message.toString)
       }
 
       def change_command(f: Document.State => (Command.State, Document.State))
       {
         try {
           val st = global_state.change_result(f)
           change_buffer.invoke(false, Nil, List(st.command))
         }
         catch { case _: Document.State.Fail => bad_output() }
       }
 
       output match {
         case msg: Prover.Protocol_Output =>
           val handled = protocol_handlers.invoke(msg)
           if (!handled) {
             msg.properties match {
               case Markup.Protocol_Handler(name) if prover.defined =>
                 init_protocol_handler(name)
 
               case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
                 command_timings.post(Session.Command_Timing(props))
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
                 change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))
 
               case Markup.ML_Statistics(props) =>
                 runtime_statistics.post(Session.Runtime_Statistics(props))
 
               case Markup.Task_Statistics(props) =>
                 task_statistics.post(Session.Task_Statistics(props))
 
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
-                if (session_options.bool("pide_exports")) {
-                  val id = Value.Long.unapply(args.id.get).get
-                  val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
-                  change_command(_.add_export(id, (args.serial, export)))
-                }
+                val id = Value.Long.unapply(args.id.get).get
+                val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
+                change_command(_.add_export(id, (args.serial, export)))
 
               case List(Markup.Commands_Accepted.PROPERTY) =>
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
                     ids.foreach(id =>
                       change_command(_.accumulate(id, Protocol.Commands_Accepted.message, xml_cache)))
                   case _ => bad_output()
                 }
 
               case List(Markup.Assign_Update.PROPERTY) =>
                 msg.text match {
                   case Protocol.Assign_Update(id, edited, update) =>
                     try {
                       val (edited_nodes, cmds) =
                         global_state.change_result(_.assign(id, edited, update))
                       change_buffer.invoke(true, edited_nodes, cmds)
                       manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
                   case _ => bad_output()
                 }
                 delay_prune.invoke()
 
               case List(Markup.Removed_Versions.PROPERTY) =>
                 msg.text match {
                   case Protocol.Removed(removed) =>
                     try {
                       global_state.change(_.removed_versions(removed))
                       manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
                   case _ => bad_output()
                 }
 
               case _ => bad_output()
             }
           }
         case _ =>
           output.properties match {
             case Position.Id(state_id) =>
               change_command(_.accumulate(state_id, output.message, xml_cache))
 
             case _ if output.is_init =>
               prover.get.options(file_formats.prover_options(session_options))
               prover.get.init_session(resources)
               phase = Session.Ready
               debugger.ready()
 
             case Markup.Process_Result(result) if output.is_exit =>
               file_formats.stop_session
               phase = Session.Terminated(result)
               prover.reset
 
             case _ =>
               raw_output_messages.post(output)
           }
         }
     }
     //}}}
 
 
     /* main thread */
 
     Consumer_Thread.fork[Any]("Session.manager", daemon = true)
     {
       case arg: Any =>
         //{{{
         arg match {
           case output: Prover.Output =>
             if (output.is_syslog) {
               syslog += output.message
               syslog_messages.post(output)
             }
 
             if (output.is_stdout || output.is_stderr)
               raw_output_messages.post(output)
             else handle_output(output)
 
             all_messages.post(output)
 
           case input: Prover.Input =>
             all_messages.post(input)
 
           case Start(start_prover) if !prover.defined =>
             prover.set(start_prover(manager.send(_)))
 
           case Stop =>
             consolidation.exit()
             delay_prune.revoke()
             if (prover.defined) {
               protocol_handlers.exit()
               global_state.change(_ => Document.State.init)
               prover.get.terminate
             }
 
           case Get_State(promise) =>
             promise.fulfill(global_state.value)
 
           case Consolidate_Execution =>
             if (prover.defined) {
               val state = global_state.value
               state.stable_tip_version match {
                 case None => consolidation.update()
                 case Some(version) =>
                   val consolidate =
                     consolidation.flush().iterator.filter(name =>
                       !resources.session_base.loaded_theory(name) &&
                       !state.node_consolidated(version, name) &&
                       state.node_maybe_consolidated(version, name)).toList
                   if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate)
               }
             }
 
           case Prune_History =>
             if (prover.defined) {
               val old_versions = global_state.change_result(_.remove_versions(prune_size))
               if (old_versions.nonEmpty) prover.get.remove_versions(old_versions)
             }
 
           case Update_Options(options) =>
             if (prover.defined && is_ready) {
               prover.get.options(file_formats.prover_options(options))
               handle_raw_edits()
             }
             global_options.post(Session.Global_Options(options))
 
           case Cancel_Exec(exec_id) if prover.defined =>
             prover.get.cancel_exec(exec_id)
 
           case Session.Raw_Edits(doc_blobs, edits) if prover.defined =>
             handle_raw_edits(doc_blobs = doc_blobs, edits = edits)
 
           case Session.Dialog_Result(id, serial, result) if prover.defined =>
             prover.get.dialog_result(serial, result)
             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
 
           case Protocol_Command(name, args) if prover.defined =>
             prover.get.protocol_command_args(name, args)
 
           case change: Session.Change if prover.defined =>
             val state = global_state.value
             if (!state.removing_versions && state.is_assigned(change.previous))
               handle_change(change)
             else postponed_changes.store(change)
 
           case Session.Change_Flush if prover.defined =>
             val state = global_state.value
             if (!state.removing_versions)
               postponed_changes.flush(state).foreach(handle_change)
 
           case bad =>
             if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
         }
         true
         //}}}
     }
   }
 
 
   /* main operations */
 
   def get_state(): Document.State =
   {
     if (manager.is_active) {
       val promise = Future.promise[Document.State]
       manager.send_wait(Get_State(promise))
       promise.join
     }
     else Document.State.init
   }
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
     get_state().snapshot(name, pending_edits)
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
     resources.session_base.overall_syntax
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot =
   {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
       output_delay.sleep
       await_stable_snapshot()
     }
     else snapshot
   }
 
   def start(start_prover: Prover.Receiver => Prover)
   {
     file_formats
     _phase.change(
       {
         case Session.Inactive =>
           manager.send(Start(start_prover))
           post_phase(Session.Startup)
         case phase => error("Cannot start prover in phase " + quote(phase.print))
       })
   }
 
   def stop(): Process_Result =
   {
     val was_ready =
       _phase.guarded_access(
         {
           case Session.Startup | Session.Shutdown => None
           case Session.Terminated(_) => Some((false, phase))
           case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
           case Session.Ready => Some((true, post_phase(Session.Shutdown)))
         })
     if (was_ready) manager.send(Stop)
     prover.await_reset()
 
     change_parser.shutdown()
     change_buffer.shutdown()
     manager.shutdown()
     dispatcher.shutdown()
 
     phase match {
       case Session.Terminated(result) => result
       case phase => error("Bad session phase after shutdown: " + quote(phase.print))
     }
   }
 
   def protocol_command(name: String, args: String*)
   { manager.send(Protocol_Command(name, args.toList)) }
 
   def cancel_exec(exec_id: Document_ID.Exec)
   { manager.send(Cancel_Exec(exec_id)) }
 
   def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   {
     if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits))
   }
 
   def update_options(options: Options)
   { manager.send_wait(Update_Options(options)) }
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   { manager.send(Session.Dialog_Result(id, serial, result)) }
 }
diff --git a/src/Pure/Thy/sessions.scala b/src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala
+++ b/src/Pure/Thy/sessions.scala
@@ -1,1309 +1,1309 @@
 /*  Title:      Pure/Thy/sessions.scala
     Author:     Makarius
 
 Cumulative session information.
 */
 
 package isabelle
 
 import java.io.{File => JFile}
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
 
 import scala.collection.{SortedSet, SortedMap}
 import scala.collection.mutable
 
 
 object Sessions
 {
   /* session and theory names */
 
   val root_name: String = "ROOT"
   val theory_name: String = "Pure.Sessions"
 
   val UNSORTED = "Unsorted"
   val DRAFT = "Draft"
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
 
   def exclude_session(name: String): Boolean = name == "" || name == DRAFT
 
   def exclude_theory(name: String): Boolean =
     name == root_name || name == "README" || name == "index" || name == "bib"
 
 
   /* base info and source dependencies */
 
   object Base
   {
     def bootstrap(
         session_directories: Map[JFile, String],
         global_theories: Map[String, String]): Base =
       Base(
         session_directories = session_directories,
         global_theories = global_theories,
         overall_syntax = Thy_Header.bootstrap_syntax)
   }
 
   sealed case class Base(
     pos: Position.T = Position.none,
     doc_names: List[String] = Nil,
     session_directories: Map[JFile, String] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[(Document.Node.Name, Options)] = Nil,
     known_theories: Map[String, Document.Node.Entry] = Map.empty,
     known_loaded_files: Map[String, List[Path]] = Map.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
     errors: List[String] = Nil,
     imports: Option[Base] = None)
   {
     override def toString: String =
       "Sessions.Base(loaded_theories = " + loaded_theories.size +
         ", used_theories = " + used_theories.length + ")"
 
     def theory_qualifier(name: String): String =
       global_theories.getOrElse(name, Long_Name.qualifier(name))
     def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
 
     def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
     def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
 
     def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
       if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
     def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
       loaded_theory_syntax(name.theory)
 
     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
 
     def get_imports: Base =
       imports getOrElse Base.bootstrap(session_directories, global_theories)
   }
 
   sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base])
   {
     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
 
     def is_empty: Boolean = session_bases.isEmpty
     def apply(name: String): Base = session_bases(name)
     def get(name: String): Option[Base] = session_bases.get(name)
 
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
     def sources(name: String): List[SHA1.Digest] =
       session_bases(name).sources.map(_._2)
 
     def errors: List[String] =
       (for {
         (name, base) <- session_bases.iterator
         if base.errors.nonEmpty
       } yield cat_lines(base.errors) +
           "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos)
       ).toList
 
     def check_errors: Deps =
       errors match {
         case Nil => this
         case errs => error(cat_lines(errs))
       }
   }
 
   def deps(sessions_structure: Structure,
       progress: Progress = new Progress,
       inlined_files: Boolean = false,
       verbose: Boolean = false,
       list_files: Boolean = false,
       check_keywords: Set[String] = Set.empty): Deps =
   {
     var cache_sources = Map.empty[JFile, SHA1.Digest]
     def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] =
     {
       for {
         path <- paths
         file = path.file
         if cache_sources.isDefinedAt(file) || file.isFile
       }
       yield {
         cache_sources.get(file) match {
           case Some(digest) => (path, digest)
           case None =>
             val digest = SHA1.digest(file)
             cache_sources = cache_sources + (file -> digest)
             (path, digest)
         }
       }
     }
 
     val doc_names = Doc.doc_names()
 
     val bootstrap =
       Sessions.Base.bootstrap(
         sessions_structure.session_directories,
         sessions_structure.global_theories)
 
     val session_bases =
       (Map("" -> bootstrap) /: sessions_structure.imports_topological_order)({
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
           val info = sessions_structure(session_name)
           try {
             val parent_base = session_bases(info.parent.getOrElse(""))
 
             val imports_base: Sessions.Base =
             {
               val imports_bases = info.imports.map(session_bases(_))
               parent_base.copy(
                 known_theories =
                   (parent_base.known_theories /:
                     (for {
                       base <- imports_bases.iterator
                       (_, entry) <- base.known_theories.iterator
                     } yield (entry.name.theory -> entry)))(_ + _),
                 known_loaded_files =
                   (parent_base.known_loaded_files /:
                     imports_bases.iterator.map(_.known_loaded_files))(_ ++ _))
             }
 
             val resources = new Resources(sessions_structure, imports_base)
 
             if (verbose || list_files) {
               val groups =
                 if (info.groups.isEmpty) ""
                 else info.groups.mkString(" (", " ", ")")
               progress.echo("Session " + info.chapter + "/" + info.name + groups)
             }
 
             val dependencies = resources.session_dependencies(info)
 
             val overall_syntax = dependencies.overall_syntax
 
             val theory_files = dependencies.theories.map(_.path)
             val loaded_files =
               if (inlined_files) dependencies.loaded_files(Sessions.is_pure(info.name))
               else Nil
 
             val session_files =
               (theory_files ::: loaded_files.flatMap(_._2) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
 
             val imported_files = if (inlined_files) dependencies.imported_files else Nil
 
             if (list_files)
               progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
 
             if (check_keywords.nonEmpty) {
               Check_Keywords.check_keywords(
                 progress, overall_syntax.keywords, check_keywords, theory_files)
             }
 
             val session_graph_display: Graph_Display.Graph =
             {
               def session_node(name: String): Graph_Display.Node =
                 Graph_Display.Node("[" + name + "]", "session." + name)
 
               def node(name: Document.Node.Name): Graph_Display.Node =
               {
                 val qualifier = imports_base.theory_qualifier(name)
                 if (qualifier == info.name)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
                 else session_node(qualifier)
               }
 
               val required_sessions =
                 dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory))
                   .map(theory => imports_base.theory_qualifier(theory))
                   .filter(name => name != info.name && sessions_structure.defined(name))
 
               val required_subgraph =
                 sessions_structure.imports_graph
                   .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet)
                   .transitive_closure
                   .restrict(required_sessions.toSet)
                   .transitive_reduction_acyclic
 
               val graph0 =
                 (Graph_Display.empty_graph /: required_subgraph.topological_order)(
                   { case (g, session) =>
                       val a = session_node(session)
                       val bs = required_subgraph.imm_preds(session).toList.map(session_node)
                       ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
 
               (graph0 /: dependencies.entries)(
                 { case (g, entry) =>
                     val a = node(entry.name)
                     val bs = entry.header.imports.map(node).filterNot(_ == a)
                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
             }
 
             val known_theories =
               (imports_base.known_theories /:
                 dependencies.entries.iterator.map(entry => entry.name.theory -> entry))(_ + _)
 
             val known_loaded_files = imports_base.known_loaded_files ++ loaded_files
 
             val used_theories =
               for ((options, name) <- dependencies.adjunct_theories)
               yield (name, options)
 
             def used_theories_session_iterator: Iterator[Document.Node.Name] =
               for {
                 (name, _) <- used_theories.iterator
                 if imports_base.theory_qualifier(name) == session_name
               } yield name
 
             val dir_errors =
             {
               val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
                   name <- used_theories_session_iterator
                   path = name.master_dir_path
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
                 } yield (path1, name)).toList
               val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
 
               val errs1 =
                 for { (path1, name) <- bad }
                 yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString)
               val errs2 =
                 if (bad_dirs.isEmpty) Nil
                 else List("Implicit use of session directories: " + commas(bad_dirs))
               val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
               val errs4 =
                 (for {
                   name <- used_theories_session_iterator
                   name1 <- resources.find_theory_node(name.theory)
                   if name.node != name1.node
                 } yield "Incoherent theory file import:\n  " + name.path + " vs. \n  " + name1.path)
                 .toList
 
               errs1 ::: errs2 ::: errs3 ::: errs4
             }
 
             val sources_errors =
               for (p <- session_files if !p.is_file) yield "No such file: " + p
 
             val path_errors =
               try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
               catch { case ERROR(msg) => List(msg) }
 
             val bibtex_errors =
               try { info.bibtex_entries; Nil }
               catch { case ERROR(msg) => List(msg) }
 
             val base =
               Base(
                 pos = info.pos,
                 doc_names = doc_names,
                 session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = used_theories,
                 known_theories = known_theories,
                 known_loaded_files = known_loaded_files,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
                 sources = check_sources(session_files),
                 session_graph_display = session_graph_display,
                 errors = dependencies.errors ::: dir_errors ::: sources_errors :::
                   path_errors ::: bibtex_errors,
                 imports = Some(imports_base))
 
             session_bases + (info.name -> base)
           }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred in session " +
                 quote(info.name) + Position.here(info.pos))
           }
       })
 
     Deps(sessions_structure, session_bases)
   }
 
 
   /* base info */
 
   sealed case class Base_Info(
     session: String,
     sessions_structure: Structure,
     errors: List[String],
     base: Base,
     infos: List[Info])
   {
     def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
   }
 
   def base_info(options: Options,
     session: String,
     progress: Progress = new Progress,
     dirs: List[Path] = Nil,
     include_sessions: List[String] = Nil,
     session_ancestor: Option[String] = None,
     session_requirements: Boolean = false): Base_Info =
   {
     val full_sessions = load_structure(options, dirs = dirs)
 
     val selected_sessions =
       full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
     val info = selected_sessions(session)
     val ancestor = session_ancestor orElse info.parent
 
     val (session1, infos1) =
       if (session_requirements && ancestor.isDefined) {
         val deps = Sessions.deps(selected_sessions, progress = progress)
         val base = deps(session)
 
         val ancestor_loaded =
           deps.get(ancestor.get) match {
             case Some(ancestor_base)
             if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
               ancestor_base.loaded_theories.defined _
             case _ =>
               error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
           }
 
         val required_theories =
           for {
             thy <- base.loaded_theories.keys
             if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session
           }
           yield thy
 
         if (required_theories.isEmpty) (ancestor.get, Nil)
         else {
           val other_name = info.name + "_requirements(" + ancestor.get + ")"
           Isabelle_System.isabelle_tmp_prefix()
 
           (other_name,
             List(
               make_info(info.options,
                 dir_selected = false,
                 dir = Path.explode("$ISABELLE_TMP_PREFIX"),
                 chapter = info.chapter,
                 Session_Entry(
                   pos = info.pos,
                   name = other_name,
                   groups = info.groups,
                   path = ".",
                   parent = ancestor,
                   description = "Required theory imports from other sessions",
                   options = Nil,
                   imports = info.deps,
                   directories = Nil,
                   theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
                   document_files = Nil,
                   export_files = Nil))))
         }
       }
       else (session, Nil)
 
     val full_sessions1 =
       if (infos1.isEmpty) full_sessions
       else load_structure(options, dirs = dirs, infos = infos1)
 
     val selected_sessions1 =
       full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions))
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
     Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1)
   }
 
 
   /* cumulative session info */
 
   sealed case class Info(
     name: String,
     chapter: String,
     dir_selected: Boolean,
     pos: Position.T,
     groups: List[String],
     dir: Path,
     parent: Option[String],
     description: String,
     directories: List[Path],
     options: Options,
     imports: List[String],
     theories: List[(Options, List[(String, Position.T)])],
     global_theories: List[String],
     document_files: List[(Path, Path)],
     export_files: List[(Path, Int, List[String])],
     meta_digest: SHA1.Digest)
   {
     def deps: List[String] = parent.toList ::: imports
 
     def dirs: List[Path] = dir :: directories
 
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
     def bibtex_entries: List[Text.Info[String]] =
       (for {
         (document_dir, file) <- document_files.iterator
         if Bibtex.is_bibtex(file.file_name)
         info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
       } yield info).toList
 
     def record_proofs: Boolean = options.int("record_proofs") >= 2
 
     def is_afp: Boolean = chapter == AFP.chapter
     def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains)
   }
 
   def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String,
     entry: Session_Entry): Info =
   {
     try {
       val name = entry.name
 
       if (exclude_session(name)) error("Bad session name")
       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
       val session_path = dir + Path.explode(entry.path)
       val directories = entry.directories.map(dir => session_path + Path.explode(dir))
 
       val session_options = options ++ entry.options
 
       val theories =
         entry.theories.map({ case (opts, thys) =>
           (session_options ++ opts,
             thys.map({ case ((thy, pos), _) =>
               if (exclude_theory(thy))
                 error("Bad theory name " + quote(thy) + Position.here(pos))
               else (thy, pos) })) })
 
       val global_theories =
         for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
         yield {
           val thy_name = Path.explode(thy).file_name
           if (Long_Name.is_qualified(thy_name))
             error("Bad qualified name for global theory " +
               quote(thy_name) + Position.here(pos))
           else thy_name
         }
 
       val conditions =
         theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
           map(x => (x, Isabelle_System.getenv(x) != ""))
 
       val document_files =
         entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
 
       val export_files =
         entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) })
 
       val meta_digest =
         SHA1.digest((name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
           entry.theories_no_position, conditions, entry.document_files).toString)
 
       Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path,
         entry.parent, entry.description, directories, session_options,
         entry.imports, theories, global_theories, document_files, export_files, meta_digest)
     }
     catch {
       case ERROR(msg) =>
         error(msg + "\nThe error(s) above occurred in session entry " +
           quote(entry.name) + Position.here(entry.pos))
     }
   }
 
   object Selection
   {
     val empty: Selection = Selection()
     val all: Selection = Selection(all_sessions = true)
     def session(session: String): Selection = Selection(sessions = List(session))
   }
 
   sealed case class Selection(
     requirements: Boolean = false,
     all_sessions: Boolean = false,
     base_sessions: List[String] = Nil,
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
     sessions: List[String] = Nil)
   {
     def ++ (other: Selection): Selection =
       Selection(
         requirements = requirements || other.requirements,
         all_sessions = all_sessions || other.all_sessions,
         base_sessions = Library.merge(base_sessions, other.base_sessions),
         exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
         exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
         session_groups = Library.merge(session_groups, other.session_groups),
         sessions = Library.merge(sessions, other.sessions))
   }
 
   def make(infos: List[Info]): Structure =
   {
     def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
       : Graph[String, Info] =
     {
       def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) =
       {
         if (!g.defined(parent))
           error("Bad " + kind + " session " + quote(parent) + " for " +
             quote(name) + Position.here(pos))
 
         try { g.add_edge_acyclic(parent, name) }
         catch {
           case exn: Graph.Cycles[_] =>
             error(cat_lines(exn.cycles.map(cycle =>
               "Cyclic session dependency of " +
                 cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
         }
       }
       (graph /: graph.iterator) {
         case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _))
       }
     }
 
     val info_graph =
       (Graph.string[Info] /: infos) {
         case (graph, info) =>
           if (graph.defined(info.name))
             error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
               Position.here(graph.get_node(info.name).pos))
           else graph.new_node(info.name, info)
       }
     val build_graph = add_edges(info_graph, "parent", _.parent)
     val imports_graph = add_edges(build_graph, "imports", _.imports)
 
     val session_positions: List[(String, Position.T)] =
       (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
 
     val session_directories: Map[JFile, String] =
       (Map.empty[JFile, String] /:
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
           dir <- info.dirs.iterator
         } yield (info, dir)))({ case (dirs, (info, dir)) =>
             val session = info.name
             val canonical_dir = dir.canonical_file
             dirs.get(canonical_dir) match {
               case Some(session1) =>
                 val info1 = info_graph.get_node(session1)
                 error("Duplicate use of directory " + dir +
                   "\n  for session " + quote(session1) + Position.here(info1.pos) +
                   "\n  vs. session " + quote(session) + Position.here(info.pos))
               case None => dirs + (canonical_dir -> session)
             }
           })
 
     val global_theories: Map[String, String] =
       (Thy_Header.bootstrap_global_theories.toMap /:
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
           thy <- info.global_theories.iterator }
          yield (info, thy)))({ case (global, (info, thy)) =>
             val qualifier = info.name
             global.get(thy) match {
               case Some(qualifier1) if qualifier != qualifier1 =>
                 error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
               case _ => global + (thy -> qualifier)
             }
           })
 
     new Structure(
       session_positions, session_directories, global_theories, build_graph, imports_graph)
   }
 
   final class Structure private[Sessions](
       val session_positions: List[(String, Position.T)],
       val session_directories: Map[JFile, String],
       val global_theories: Map[String, String],
       val build_graph: Graph[String, Info],
       val imports_graph: Graph[String, Info])
   {
     sessions_structure =>
 
     def dest_session_directories: List[(String, String)] =
       for ((file, session) <- session_directories.toList)
         yield (File.standard_path(file), session)
 
     lazy val chapters: SortedMap[String, List[Info]] =
       (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
         { case (chs, (_, (info, _))) =>
             chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) })
 
     def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
 
     def defined(name: String): Boolean = imports_graph.defined(name)
     def apply(name: String): Info = imports_graph.get_node(name)
     def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
 
     def theory_qualifier(name: String): String =
       global_theories.getOrElse(name, Long_Name.qualifier(name))
 
     def check_sessions(names: List[String])
     {
       val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
       if (bad_sessions.nonEmpty)
         error("Undefined session(s): " + commas_quote(bad_sessions))
     }
 
     def check_sessions(sel: Selection): Unit =
       check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
 
     private def selected(graph: Graph[String, Info], sel: Selection): List[String] =
     {
       check_sessions(sel)
 
       val select_group = sel.session_groups.toSet
       val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
 
       val selected0 =
         if (sel.all_sessions) graph.keys
         else {
           (for {
             (name, (info, _)) <- graph.iterator
             if info.dir_selected || select_session(name) ||
               graph.get_node(name).groups.exists(select_group)
           } yield name).toList
         }
 
       if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
       else selected0
     }
 
     def selection(sel: Selection): Structure =
     {
       check_sessions(sel)
 
       val excluded =
       {
         val exclude_group = sel.exclude_session_groups.toSet
         val exclude_group_sessions =
           (for {
             (name, (info, _)) <- imports_graph.iterator
             if imports_graph.get_node(name).groups.exists(exclude_group)
           } yield name).toList
         imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
       }
 
       def restrict(graph: Graph[String, Info]): Graph[String, Info] =
       {
         val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
       new Structure(
         session_positions, session_directories, global_theories,
         restrict(build_graph), restrict(imports_graph))
     }
 
     def selection_deps(
       options: Options,
       selection: Selection,
       progress: Progress = new Progress,
       loading_sessions: Boolean = false,
       inlined_files: Boolean = false,
       verbose: Boolean = false): Deps =
     {
       val deps =
         Sessions.deps(sessions_structure.selection(selection),
           progress = progress, inlined_files = inlined_files, verbose = verbose)
 
       if (loading_sessions) {
         val selection_size = deps.sessions_structure.build_graph.size
         if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
       }
 
       deps
     }
 
     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
     def build_topological_order: List[String] = build_graph.topological_order
 
     def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse
     def imports_topological_order: List[String] = imports_graph.topological_order
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
   }
 
 
   /* parser */
 
   val ROOT: Path = Path.explode("ROOT")
   val ROOTS: Path = Path.explode("ROOTS")
 
   private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
   private val DESCRIPTION = "description"
   private val DIRECTORIES = "directories"
   private val OPTIONS = "options"
   private val SESSIONS = "sessions"
   private val THEORIES = "theories"
   private val GLOBAL = "global"
   private val DOCUMENT_FILES = "document_files"
   private val EXPORT_FILES = "export_files"
 
   val root_syntax: Outer_Syntax =
     Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
       GLOBAL + IN +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
       (DIRECTORIES, Keyword.QUASI_COMMAND) +
       (OPTIONS, Keyword.QUASI_COMMAND) +
       (SESSIONS, Keyword.QUASI_COMMAND) +
       (THEORIES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_FILES, Keyword.QUASI_COMMAND) +
       (EXPORT_FILES, Keyword.QUASI_COMMAND)
 
   abstract class Entry
   sealed case class Chapter(name: String) extends Entry
   sealed case class Session_Entry(
     pos: Position.T,
     name: String,
     groups: List[String],
     path: String,
     parent: Option[String],
     description: String,
     options: List[Options.Spec],
     imports: List[String],
     directories: List[String],
     theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
     document_files: List[(String, String)],
     export_files: List[(String, Int, List[String])]) extends Entry
   {
     def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
       theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
   }
 
   private object Parser extends Options.Parser
   {
     private val chapter: Parser[Chapter] =
     {
       val chapter_name = atom("chapter name", _.is_name)
 
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
     }
 
     private val session_entry: Parser[Session_Entry] =
     {
       val option =
         option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
           { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
       val theory_entry =
         position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }
 
       val theories =
         $$$(THEORIES) ~!
           ((options | success(Nil)) ~ rep1(theory_entry)) ^^
           { case _ ~ (x ~ y) => (x, y) }
 
       val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x }
 
       val document_files =
         $$$(DOCUMENT_FILES) ~!
           ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
 
       val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0)
 
       val export_files =
         $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
           { case _ ~ (x ~ y ~ z) => (x, y, z) }
 
       command(SESSION) ~!
         (position(session_name) ~
           (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
           ($$$("=") ~!
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep(theories) ~
               (rep(document_files) ^^ (x => x.flatten)) ~
               (rep(export_files))))) ^^
         { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k) }
     }
 
     def parse_root(path: Path): List[Entry] =
     {
       val toks = Token.explode(root_syntax.keywords, File.read(path))
       val start = Token.Pos.file(path.implode)
 
       parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
     }
   }
 
   def parse_root(path: Path): List[Entry] = Parser.parse_root(path)
 
   def parse_root_entries(path: Path): List[Session_Entry] =
     for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry])
     yield entry.asInstanceOf[Session_Entry]
 
   def read_root(options: Options, select: Boolean, path: Path): List[Info] =
   {
     var entry_chapter = UNSORTED
     val infos = new mutable.ListBuffer[Info]
     parse_root(path).foreach {
       case Chapter(name) => entry_chapter = name
       case entry: Session_Entry =>
         infos += make_info(options, select, path.dir, entry_chapter, entry)
     }
     infos.toList
   }
 
   def parse_roots(roots: Path): List[String] =
   {
     for {
       line <- split_lines(File.read(roots))
       if !(line == "" || line.startsWith("#"))
     } yield line
   }
 
 
   /* load sessions from certain directories */
 
   private def is_session_dir(dir: Path): Boolean =
     (dir + ROOT).is_file || (dir + ROOTS).is_file
 
   private def check_session_dir(dir: Path): Path =
     if (is_session_dir(dir)) File.pwd() + dir.expand
     else error("Bad session root directory: " + dir.toString)
 
   def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
   {
     val default_dirs = Isabelle_System.components().filter(is_session_dir)
     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
     yield (select, dir.canonical)
   }
 
   def load_structure(options: Options,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Info] = Nil): Structure =
   {
     def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
       load_root(select, dir) ::: load_roots(select, dir)
 
     def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] =
     {
       val root = dir + ROOT
       if (root.is_file) List((select, root)) else Nil
     }
 
     def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] =
     {
       val roots = dir + ROOTS
       if (roots.is_file) {
         for {
           entry <- parse_roots(roots)
           dir1 =
             try { check_session_dir(dir + Path.explode(entry)) }
             catch {
               case ERROR(msg) =>
                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
             }
           res <- load_dir(select, dir1)
         } yield res
       }
       else Nil
     }
 
     val roots =
       for {
         (select, dir) <- directories(dirs, select_dirs)
         res <- load_dir(select, check_session_dir(dir))
       } yield res
 
     val unique_roots =
       ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) =>
         val file = path.canonical_file
         m.get(file) match {
           case None => m + (file -> (select, path))
           case Some((select1, path1)) => m + (file -> (select1 || select, path1))
         }
       }).toList.map(_._2)
 
     make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos)
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions", args =>
   {
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     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 exclude_sessions: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle sessions [OPTIONS] [SESSIONS ...]
 
   Options are:
     -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
     -d DIR       include session directory
     -g NAME      select session group NAME
     -x NAME      exclude session NAME and all descendants
 
   Explore the structure of Isabelle sessions and print result names in
   topological order (on stdout).
 """,
       "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),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
     val sessions = getopts(args)
 
     val options = Options.init()
 
     val selection =
       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 sessions_structure =
       load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
 
     for (name <- sessions_structure.imports_topological_order) {
       Output.writeln(name, stdout = true)
     }
   })
 
 
 
   /** heap file with SHA1 digest **/
 
   private val sha1_prefix = "SHA1:"
 
   def read_heap_digest(heap: Path): Option[String] =
   {
     if (heap.is_file) {
       using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file =>
       {
         val len = file.size
         val n = sha1_prefix.length + SHA1.digest_length
         if (len >= n) {
           file.position(len - n)
 
           val buf = ByteBuffer.allocate(n)
           var i = 0
           var m = 0
           do {
             m = file.read(buf)
             if (m != -1) i += m
           }
           while (m != -1 && n > i)
 
           if (i == n) {
             val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
             val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
             if (prefix == sha1_prefix) Some(s) else None
           }
           else None
         }
         else None
       })
     }
     else None
   }
 
   def write_heap_digest(heap: Path): String =
     read_heap_digest(heap) match {
       case None =>
         val s = SHA1.digest(heap).rep
         File.append(heap, sha1_prefix + s)
         s
       case Some(s) => s
     }
 
 
 
   /** persistent store **/
 
   object Session_Info
   {
     val session_name = SQL.Column.string("session_name").make_primary_key
 
     // Build_Log.Session_Info
     val session_timing = SQL.Column.bytes("session_timing")
     val command_timings = SQL.Column.bytes("command_timings")
     val theory_timings = SQL.Column.bytes("theory_timings")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
     val task_statistics = SQL.Column.bytes("task_statistics")
     val errors = SQL.Column.bytes("errors")
     val build_log_columns =
       List(session_name, session_timing, command_timings, theory_timings,
         ml_statistics, task_statistics, errors)
 
     // Build.Session_Info
     val sources = SQL.Column.string("sources")
     val input_heaps = SQL.Column.string("input_heaps")
     val output_heap = SQL.Column.string("output_heap")
     val return_code = SQL.Column.int("return_code")
     val build_columns = List(sources, input_heaps, output_heap, return_code)
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
   }
 
   def store(options: Options): Store = new Store(options)
 
   class Store private[Sessions](val options: Options)
   {
     override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
 
+    val xml_cache: XML.Cache = XML.make_cache()
+    val xz_cache: XZ.Cache = XZ.make_cache()
+
 
     /* directories */
 
     val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
     val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
 
     def system_heaps: Boolean = options.bool("system_heaps")
 
     val output_dir: Path =
       if (system_heaps) system_output_dir else user_output_dir
 
     val input_dirs: List[Path] =
       if (system_heaps) List(system_output_dir)
       else List(user_output_dir, system_output_dir)
 
     val browser_info: Path =
       if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
       else Path.explode("$ISABELLE_BROWSER_INFO")
 
 
     /* file names */
 
     def heap(name: String): Path = Path.basic(name)
     def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
     def log(name: String): Path = Path.basic("log") + Path.basic(name)
     def log_gz(name: String): Path = log(name).ext("gz")
 
     def output_heap(name: String): Path = output_dir + heap(name)
     def output_database(name: String): Path = output_dir + database(name)
     def output_log(name: String): Path = output_dir + log(name)
     def output_log_gz(name: String): Path = output_dir + log_gz(name)
 
     def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
 
 
     /* heap */
 
     def find_heap(name: String): Option[Path] =
       input_dirs.map(_ + heap(name)).find(_.is_file)
 
     def find_heap_digest(name: String): Option[String] =
       find_heap(name).flatMap(read_heap_digest)
 
     def the_heap(name: String): Path =
       find_heap(name) getOrElse
         error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
           cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
 
 
     /* database */
 
     private def database_server: Boolean = options.bool("build_database_server")
 
     def access_database(name: String, output: Boolean = false): Option[SQL.Database] =
     {
       if (database_server) {
         val db =
           PostgreSQL.open_database(
             user = options.string("build_database_user"),
             password = options.string("build_database_password"),
             database = options.string("build_database_name"),
             host = options.string("build_database_host"),
             port = options.int("build_database_port"),
             ssh =
               options.proper_string("build_database_ssh_host").map(ssh_host =>
                 SSH.open_session(options,
                   host = ssh_host,
                   user = options.string("build_database_ssh_user"),
                   port = options.int("build_database_ssh_port"))),
             ssh_close = true)
         if (output || has_session_info(db, name)) Some(db) else { db.close; None }
       }
       else if (output) Some(SQLite.open_database(output_database(name)))
       else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database)
     }
 
     def open_database(name: String, output: Boolean = false): SQL.Database =
       access_database(name, output = output) getOrElse
         error("Missing build database for session " + quote(name))
 
     def clean_output(name: String): (Boolean, Boolean) =
     {
       val relevant_db =
         database_server &&
         {
           access_database(name) match {
             case Some(db) =>
               try {
                 db.transaction {
                   val relevant_db = has_session_info(db, name)
                   init_session_info(db, name)
                   relevant_db
                 }
               } finally { db.close }
             case None => false
           }
         }
 
       val del =
         for {
           dir <-
             (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
           file <- List(heap(name), database(name), log(name), log_gz(name))
           path = dir + file if path.is_file
         } yield path.file.delete
 
       val relevant = relevant_db || del.nonEmpty
       val ok = del.forall(b => b)
       (relevant, ok)
     }
 
 
     /* SQL database content */
 
-    val xml_cache: XML.Cache = XML.make_cache()
-    val xz_cache: XZ.Cache = XZ.make_cache()
-
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
       db.using_statement(Session_Info.table.select(List(column),
         Session_Info.session_name.where_equal(name)))(stmt =>
       {
         val res = stmt.execute_query()
         if (!res.next()) Bytes.empty else res.bytes(column)
       })
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
       Properties.uncompress(
         read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache))
 
 
     /* session info */
 
     def init_session_info(db: SQL.Database, name: String)
     {
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
 
         db.create_table(Export.Data.table)
         db.using_statement(
           Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute)
       }
     }
 
     def has_session_info(db: SQL.Database, name: String): Boolean =
     {
       db.transaction {
         db.tables.contains(Session_Info.table.name) &&
         {
           db.using_statement(
             Session_Info.table.select(List(Session_Info.session_name),
               Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
         }
       }
     }
 
     def write_session_info(
       db: SQL.Database,
       name: String,
       build_log: Build_Log.Session_Info,
       build: Build.Session_Info)
     {
       db.transaction {
         db.using_statement(Session_Info.table.insert())(stmt =>
         {
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
           stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache)
           stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache)
           stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache)
           stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache)
           stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = xz_cache)
           stmt.string(8) = build.sources
           stmt.string(9) = cat_lines(build.input_heaps)
           stmt.string(10) = build.output_heap getOrElse ""
           stmt.int(11) = build.return_code
           stmt.execute()
         })
       }
     }
 
     def read_session_timing(db: SQL.Database, name: String): Properties.T =
       Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache))
 
     def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.command_timings)
 
     def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.theory_timings)
 
     def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.ml_statistics)
 
     def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.task_statistics)
 
     def read_errors(db: SQL.Database, name: String): List[String] =
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = xz_cache)
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     {
       if (db.tables.contains(Session_Info.table.name)) {
         db.using_statement(Session_Info.table.select(Session_Info.build_columns,
           Session_Info.session_name.where_equal(name)))(stmt =>
         {
           val res = stmt.execute_query()
           if (!res.next()) None
           else {
             Some(
               Build.Session_Info(
                 res.string(Session_Info.sources),
                 split_lines(res.string(Session_Info.input_heaps)),
                 res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
                 res.int(Session_Info.return_code)))
           }
         })
       }
       else None
     }
   }
 }
diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala
+++ b/src/Pure/Tools/build.scala
@@ -1,956 +1,947 @@
 /*  Title:      Pure/Tools/build.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Build and manage Isabelle sessions.
 */
 
 package isabelle
 
 
 import scala.collection.{SortedSet, mutable}
 import scala.annotation.tailrec
 
 
 object Build
 {
   /** auxiliary **/
 
   /* persistent build info */
 
   sealed case class Session_Info(
     sources: String,
     input_heaps: List[String],
     output_heap: Option[String],
     return_code: Int)
   {
     def ok: Boolean = return_code == 0
   }
 
 
   /* queue with scheduling information */
 
   private object Queue
   {
     type Timings = (List[Properties.T], Double)
 
     def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
     {
       val no_timings: Timings = (Nil, 0.0)
 
       store.access_database(session_name) match {
         case None => no_timings
         case Some(db) =>
           def ignore_error(msg: String) =
           {
             progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
             no_timings
           }
           try {
             val command_timings = store.read_command_timings(db, session_name)
             val session_timing =
               store.read_session_timing(db, session_name) match {
                 case Markup.Elapsed(t) => t
                 case _ => 0.0
               }
             (command_timings, session_timing)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
             case _: XML.Error => ignore_error("")
           }
           finally { db.close }
       }
     }
 
     def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
       : Map[String, Double] =
     {
       val maximals = sessions_structure.build_graph.maximals.toSet
       def desc_timing(session_name: String): Double =
       {
         if (maximals.contains(session_name)) timing(session_name)
         else {
           val descendants = sessions_structure.build_descendants(List(session_name)).toSet
           val g = sessions_structure.build_graph.restrict(descendants)
           (0.0 :: g.maximals.flatMap(desc => {
             val ps = g.all_preds(List(desc))
             if (ps.exists(p => !timing.isDefinedAt(p))) None
             else Some(ps.map(timing(_)).sum)
           })).max
         }
       }
       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
     }
 
     def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
       : Queue =
     {
       val graph = sessions_structure.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
         make_session_timing(sessions_structure,
           timings.map({ case (name, (_, t)) => (name, t) }).toMap)
 
       object Ordering extends scala.math.Ordering[String]
       {
         def compare_timing(name1: String, name2: String): Int =
         {
           val t1 = session_timing(name1)
           val t2 = session_timing(name2)
           if (t1 == 0.0 || t2 == 0.0) 0
           else t1 compare t2
         }
 
         def compare(name1: String, name2: String): Int =
           compare_timing(name2, name1) match {
             case 0 =>
               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
                 case ord => ord
               }
             case ord => ord
           }
       }
 
       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
     }
   }
 
   private class Queue(
     graph: Graph[String, Sessions.Info],
     order: SortedSet[String],
     val command_timings: String => List[Properties.T])
   {
     def is_inner(name: String): Boolean = !graph.is_maximal(name)
 
     def is_empty: Boolean = graph.is_empty
 
     def - (name: String): Queue =
       new Queue(graph.del_node(name),
         order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
         command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
     {
       val it = order.iterator.dropWhile(name =>
         skip(name)
           || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
           || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
       else None
     }
   }
 
 
   /* PIDE protocol handler */
 
   /* job: running prover process */
 
   private class Job(progress: Progress,
     session_name: String,
     val info: Sessions.Info,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_store: Boolean,
     verbose: Boolean,
     val numa_node: Option[Int],
     command_timings: List[Properties.T])
   {
     val options: Options = NUMA.policy_options(info.options, numa_node)
 
     private val sessions_structure = deps.sessions_structure
 
     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display)
 
     private val export_tmp_dir = Isabelle_System.tmp_dir("export")
     private val export_consumer =
       Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
 
     private val future_result: Future[Process_Result] =
       Future.thread("build", uninterruptible = true) {
         val parent = info.parent.getOrElse("")
         val base = deps(parent)
         val args_yxml =
           YXML.string_of_body(
             {
               import XML.Encode._
               pair(list(pair(string, int)), pair(list(properties), pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(pair(string, properties)))),
                 pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
                 pair(list(string), pair(list(pair(string, string)),
                 pair(list(string), list(string)))))))))))))))))(
               (Symbol.codes, (command_timings, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (session_name, (Path.current,
                 (info.theories,
                 (sessions_structure.session_positions,
                 (sessions_structure.dest_session_directories,
                 (base.doc_names, (base.global_theories.toList,
                 (base.loaded_theories.keys, info.bibtex_entries.map(_.info))))))))))))))))))
             })
 
         val env =
           Isabelle_System.settings() +
             ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
 
         val is_pure = Sessions.is_pure(session_name)
 
         val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
 
         val eval_store =
           if (do_store) {
             (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
             List("ML_Heap.save_child " +
               ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
           }
           else Nil
 
         if (options.bool("pide_session")) {
           val resources = new Resources(sessions_structure, deps(parent))
-          val session = new Session(options, resources)
+          val session =
+            new Session(options, resources) {
+              override val xml_cache: XML.Cache = store.xml_cache
+              override val xz_cache: XZ.Cache = store.xz_cache
+            }
 
           val build_session_errors: Promise[List[String]] = Future.promise
           val stdout = new StringBuilder(1000)
           val messages = new mutable.ListBuffer[String]
           val command_timings = new mutable.ListBuffer[Properties.T]
           val theory_timings = new mutable.ListBuffer[Properties.T]
           val runtime_statistics = new mutable.ListBuffer[Properties.T]
           val task_statistics = new mutable.ListBuffer[Properties.T]
 
+          def fun(
+            name: String,
+            acc: mutable.ListBuffer[Properties.T],
+            unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
+          {
+            name -> ((msg: Prover.Protocol_Output) =>
+              unapply(msg.properties) match {
+                case Some(props) => acc += props; true
+                case _ => false
+              })
+          }
+
           session.init_protocol_handler(new Session.Protocol_Handler
             {
               override def exit() { build_session_errors.cancel }
 
               private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
               {
                 val (rc, errors) =
                   try {
                     val (rc, errs) =
                     {
                       import XML.Decode._
                       pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
                     }
                     val errors =
                       for (err <- errs) yield {
                         val prt = Protocol_Message.expose_no_reports(err)
                         Pretty.string_of(prt, metric = Symbol.Metric)
                       }
                     (rc, errors)
                   }
                   catch { case ERROR(err) => (2, List(err)) }
 
                 session.protocol_command("Prover.stop", rc.toString)
                 build_session_errors.fulfill(errors)
                 true
               }
 
               private def loading_theory(msg: Prover.Protocol_Output): Boolean =
                 msg.properties match {
                   case Markup.Loading_Theory(name) =>
                     progress.theory(Progress.Theory(name, session = session_name))
                     true
                   case _ => false
                 }
 
               private def export(msg: Prover.Protocol_Output): Boolean =
                 msg.properties match {
                   case Protocol.Export(args) =>
                     export_consumer(session_name, args, msg.bytes)
                     true
                   case _ => false
                 }
 
-              private def command_timing(msg: Prover.Protocol_Output): Boolean =
-                msg.properties match {
-                  case Markup.Command_Timing(props) => command_timings += props; true
-                  case _ => false
-                }
-
-              private def theory_timing(msg: Prover.Protocol_Output): Boolean =
-                msg.properties match {
-                  case Markup.Theory_Timing(props) => theory_timings += props; true
-                  case _ => false
-                }
-
-              private def ml_stats(msg: Prover.Protocol_Output): Boolean =
-                msg.properties match {
-                  case Markup.ML_Statistics(props) => runtime_statistics += props; true
-                  case _ => false
-                }
-
-              private def task_stats(msg: Prover.Protocol_Output): Boolean =
-                msg.properties match {
-                  case Markup.Task_Statistics(props) => task_statistics += props; true
-                  case _ => false
-                }
-
               val functions =
                 List(
                   Markup.Build_Session_Finished.name -> build_session_finished,
                   Markup.Loading_Theory.name -> loading_theory,
                   Markup.EXPORT -> export,
-                  Markup.Command_Timing.name -> command_timing,
-                  Markup.Theory_Timing.name -> theory_timing,
-                  Markup.ML_Statistics.name -> ml_stats,
-                  Markup.Task_Statistics.name -> task_stats)
+                  fun(Markup.Command_Timing.name, command_timings, Markup.Command_Timing.unapply),
+                  fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
+                  fun(Markup.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply),
+                  fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
             })
 
           session.all_messages += Session.Consumer[Any]("build_session_output")
             {
               case msg: Prover.Output =>
                 val message = msg.message
                 if (msg.is_stdout) {
                   stdout ++= Symbol.encode(XML.content(message))
                 }
                 else if (Protocol.is_exported(message)) {
                   messages +=
                     Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))
                 }
               case _ =>
             }
 
           val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
           val process =
             Isabelle_Process(session, options, sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env)
 
           val errors =
             Isabelle_Thread.interrupt_handler(_ => process.terminate) {
               Exn.capture { process.await_startup } match {
                 case Exn.Res(_) =>
                   session.protocol_command("build_session", args_yxml)
                   build_session_errors.join_result
                 case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
               }
             }
 
           val process_result =
             Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
           val process_output =
             stdout.toString :: messages.toList :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
 
           val result = process_result.output(process_output)
 
           errors match {
             case Exn.Res(Nil) => result
             case Exn.Res(errs) =>
               result.error_rc.output(
                 errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
                   errs.map(Protocol.Error_Message_Marker.apply))
             case Exn.Exn(Exn.Interrupt()) =>
               if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
             case Exn.Exn(exn) => throw exn
           }
         }
         else {
           val args_file = Isabelle_System.tmp_file("build")
           File.write(args_file, args_yxml)
 
           val eval_build =
             "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file))
           val eval_main = Command_Line.ML_tool(eval_build :: eval_store)
 
           val process =
             ML_Process(options, deps.sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
 
           Isabelle_Thread.interrupt_handler(_ => process.terminate) {
             process.result(
               progress_stdout =
                 {
                   case Protocol.Loading_Theory_Marker(theory) =>
                     progress.theory(Progress.Theory(theory, session = session_name))
                   case Protocol.Export.Marker((args, path)) =>
                     val body =
                       try { Bytes.read(path) }
                       catch {
                         case ERROR(msg) =>
                           error("Failed to read export " + quote(args.compound_name) + "\n" + msg)
                       }
                     path.file.delete
                     export_consumer(session_name, args, body)
                   case _ =>
                 },
               progress_limit =
                 options.int("process_output_limit") match {
                   case 0 => None
                   case m => Some(m * 1000000L)
                 },
               strict = false)
           }
         }
       }
 
     def terminate: Unit = future_result.cancel
     def is_finished: Boolean = future_result.is_finished
 
     private val timeout_request: Option[Event_Timer.Request] =
     {
       if (info.timeout > Time.zero)
         Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
       else None
     }
 
     def join: (Process_Result, Option[String]) =
     {
       val result0 = future_result.join
       val result1 =
         export_consumer.shutdown(close = true).map(Output.error_message_text) match {
           case Nil => result0
           case errs => result0.errors(errs).error_rc
         }
 
       Isabelle_System.rm_tree(export_tmp_dir)
 
       if (result1.ok)
         Present.finish(progress, store.browser_info, graph_file, info, session_name)
 
       graph_file.delete
 
       val was_timeout =
         timeout_request match {
           case None => false
           case Some(request) => !request.cancel
         }
 
       val result2 =
         if (result1.interrupted) {
           if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
           else result1.error(Output.error_message_text("Interrupt"))
         }
         else result1
 
       val heap_digest =
         if (result2.ok && do_store && store.output_heap(session_name).is_file)
           Some(Sessions.write_heap_digest(store.output_heap(session_name)))
         else None
 
       (result2, heap_digest)
     }
   }
 
 
 
   /** build with results **/
 
   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   {
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def info(name: String): Sessions.Info = results(name)._2
     val rc: Int =
       (0 /: results.iterator.map(
         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
     def ok: Boolean = rc == 0
 
     override def toString: String = rc.toString
   }
 
   def build(
     options: Options,
     selection: Sessions.Selection,
     progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Sessions.Info] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     soft_build: Boolean = false,
     verbose: Boolean = false,
     export_files: Boolean = false): Results =
   {
     val build_options =
       options +
         "ML_statistics" +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
-        "pide_exports=false" +
         "pide_reports=false"
 
     val store = Sessions.store(build_options)
 
     Isabelle_Fonts.init()
 
 
     /* session selection and dependencies */
 
     val full_sessions =
       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
 
     def sources_stamp(deps: Sessions.Deps, session_name: String): String =
     {
       val digests =
         full_sessions(session_name).meta_digest ::
         deps.sources(session_name) :::
         deps.imported_sources(session_name)
       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
     }
 
     val deps =
     {
       val deps0 =
         Sessions.deps(full_sessions.selection(selection),
           progress = progress, inlined_files = true, verbose = verbose,
           list_files = list_files, check_keywords = check_keywords).check_errors
 
       if (soft_build && !fresh_build) {
         val outdated =
           deps0.sessions_structure.build_topological_order.flatMap(name =>
             store.access_database(name) match {
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
                   if build.ok && build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
                 }
               case None => Some(name)
             })
 
         Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
           progress = progress, inlined_files = true).check_errors
       }
       else deps0
     }
 
 
     /* check unknown files */
 
     if (check_unknown_files) {
       val source_files =
         (for {
           (_, base) <- deps.session_bases.iterator
           (path, _) <- base.sources.iterator
         } yield path).toList
       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
       val unknown_files =
         Mercurial.check_files(source_files)._2.
           filterNot(path => exclude_files.contains(path.canonical_file))
       if (unknown_files.nonEmpty) {
         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
       }
     }
 
 
     /* main build process */
 
     val queue = Queue(progress, deps.sessions_structure, store)
 
     store.prepare_output_dir()
 
     if (clean_build) {
       for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)
           else progress.echo(name + " FAILED to clean")
         }
       }
     }
 
     // scheduler loop
     case class Result(
       current: Boolean,
       heap_digest: Option[String],
       process: Option[Process_Result],
       info: Sessions.Info)
     {
       def ok: Boolean =
         process match {
           case None => false
           case Some(res) => res.rc == 0
         }
     }
 
     def sleep()
     {
       Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
     }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
     @tailrec def loop(
       pending: Queue,
       running: Map[String, (List[String], Job)],
       results: Map[String, Result]): Map[String, Result] =
     {
       def used_node(i: Int): Boolean =
         running.iterator.exists(
           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
 
       if (pending.is_empty) results
       else {
         if (progress.stopped) {
           for ((_, (_, job)) <- running) job.terminate
         }
 
         running.find({ case (_, (_, job)) => job.is_finished }) match {
           case Some((session_name, (input_heaps, job))) =>
             //{{{ finish job
 
             val (process_result, heap_digest) = job.join
 
             val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail =
             {
               val tail = job.info.options.int("process_output_tail")
               process_result.copy(
                 out_lines =
                   "(see also " + store.output_log(session_name).file.toString + ")" ::
                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
             }
 
 
             // write log file
             if (process_result.ok) {
               File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
             }
             else File.write(store.output_log(session_name), terminate_lines(log_lines))
 
             // write database
             {
               val build_log =
                 Build_Log.Log_File(session_name, process_result.out_lines).
                   parse_session_info(
                     command_timings = true,
                     theory_timings = true,
                     ml_statistics = true,
                     task_statistics = true)
 
               using(store.open_database(session_name, output = true))(db =>
                 store.write_session_info(db, session_name,
                   build_log =
                     if (process_result.timeout) build_log.error("Timeout") else build_log,
                   build =
                     Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
                       process_result.rc)))
             }
 
             // messages
             process_result.err_lines.foreach(progress.echo)
 
             if (process_result.ok)
               progress.echo(
                 "Finished " + session_name + " (" + process_result.timing.message_resources + ")")
             else {
               progress.echo(session_name + " FAILED")
               if (!process_result.interrupted) progress.echo(process_result_tail.out)
             }
 
             loop(pending - session_name, running - session_name,
               results +
                 (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt) match {
               case Some((session_name, info)) =>
                 val ancestor_results =
                   deps.sessions_structure.build_requirements(List(session_name)).
                     filterNot(_ == session_name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
 
                 val (current, heap_digest) =
                 {
                   store.access_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>
                           val heap_digest = store.find_heap_digest(session_name)
                           val current =
                             !fresh_build &&
                             build.ok &&
                             build.sources == sources_stamp(deps, session_name) &&
                             build.input_heaps == ancestor_heaps &&
                             build.output_heap == heap_digest &&
                             !(do_store && heap_digest.isEmpty)
                           (current, heap_digest)
                         case None => (false, None)
                       }
                     case None => (false, None)
                   }
                 }
                 val all_current = current && ancestor_results.forall(_.current)
 
                 if (all_current)
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
 
                   store.clean_output(session_name)
                   using(store.open_database(session_name, output = true))(
                     store.init_session_info(_, session_name))
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Job(progress, session_name, info, deps, store, do_store, verbose,
                       numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
                 else {
                   progress.echo(session_name + " CANCELLED")
                   loop(pending - session_name, running,
                     results + (session_name -> Result(false, heap_digest, None, info)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
             ///}}}
           case None => sleep(); loop(pending, running, results)
         }
       }
     }
 
 
     /* build results */
 
     val results0 =
       if (deps.is_empty) {
         progress.echo_warning("Nothing to build")
         Map.empty[String, Result]
       }
       else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
 
     val results =
       new Results(
         (for ((name, result) <- results0.iterator)
           yield (name, (result.process, result.info))).toMap)
 
     if (export_files) {
       for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
         val info = results.info(name)
         if (info.export_files.nonEmpty) {
           progress.echo("Exporting " + info.name + " ...")
           for ((dir, prune, pats) <- info.export_files) {
             Export.export_files(store, name, info.dir + dir,
               progress = if (verbose) progress else new Progress,
               export_prune = prune,
               export_patterns = pats)
           }
         }
       }
     }
 
     if (results.rc != 0 && (verbose || !no_build)) {
       val unfinished =
         (for {
           name <- results.sessions.iterator
           if !results(name).ok
          } yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
 
 
     /* global browser info */
 
     if (!no_build) {
       val browser_chapters =
         (for {
           (name, result) <- results0.iterator
           if result.ok
           info = full_sessions(name)
           if info.options.bool("browser_info")
         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
 
       for ((chapter, entries) <- browser_chapters)
         Present.update_chapter_index(store.browser_info, chapter, entries)
 
       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
     }
 
     results
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   {
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var numa_shuffling = false
     var requirements = false
     var soft_build = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
     var build_heap = false
     var clean_build = false
     var dirs: List[Path] = Nil
     var export_files = false
     var fresh_build = false
     var session_groups: List[String] = Nil
     var max_jobs = 1
     var check_keywords: Set[String] = Set.empty
     var list_files = false
     var no_build = false
     var options = Options.init(opts = build_options)
     var verbose = false
     var exclude_sessions: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -R           refer to requirements of selected sessions
     -S           soft build: only observe changes of sources, not heap images
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           build heap images
     -c           clean build
     -d DIR       include session directory
     -e           export files from session specification into file-system
     -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- test dependencies only
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
   Build and manage Isabelle sessions, depending on implicit settings:
 
 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
       "R" -> (_ => requirements = true),
       "S" -> (_ => soft_build = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "b" -> (_ => build_heap = true),
       "c" -> (_ => clean_build = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "e" -> (_ => export_files = true),
       "f" -> (_ => fresh_build = true),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "k:" -> (arg => check_keywords = check_keywords + arg),
       "l" -> (_ => list_files = true),
       "n" -> (_ => no_build = true),
       "o:" -> (arg => options = options + arg),
       "v" -> (_ => verbose = true),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
     val sessions = getopts(args)
 
     val progress = new Console_Progress(verbose = verbose)
 
     val start_date = Date.now()
 
     if (verbose) {
       progress.echo(
         "Started at " + Build_Log.print_date(start_date) +
           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
       progress.echo(Build_Log.Settings.show() + "\n")
     }
 
     val results =
       progress.interrupt_handler {
         build(options,
           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),
           progress = progress,
           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
           build_heap = build_heap,
           clean_build = clean_build,
           dirs = dirs,
           select_dirs = select_dirs,
           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
           max_jobs = max_jobs,
           list_files = list_files,
           check_keywords = check_keywords,
           fresh_build = fresh_build,
           no_build = no_build,
           soft_build = soft_build,
           verbose = verbose,
           export_files = export_files)
       }
     val end_date = Date.now()
     val elapsed_time = end_date.time - start_date.time
 
     if (verbose) {
       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
     }
 
     val total_timing =
       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
         copy(elapsed = elapsed_time)
     progress.echo(total_timing.message_resources)
 
     sys.exit(results.rc)
   })
 
 
   /* build logic image */
 
   def build_logic(options: Options, logic: String,
     progress: Progress = new Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
     fresh: Boolean = false,
     strict: Boolean = false): Int =
   {
     val selection = Sessions.Selection.session(logic)
     val rc =
       if (!fresh &&
           build(options, selection, build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
         Build.build(options, selection, progress = progress, build_heap = build_heap,
           fresh_build = fresh, dirs = dirs).rc
       }
     if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
   }
 }