diff --git a/src/Pure/PIDE/markup.scala b/src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala
+++ b/src/Pure/PIDE/markup.scala
@@ -1,763 +1,706 @@
 /*  Title:      Pure/PIDE/markup.scala
     Author:     Makarius
 
 Quasi-abstract markup elements.
 */
 
 package isabelle
 
 
 object Markup
 {
   /* elements */
 
   object Elements
   {
     def apply(elems: Set[String]): Elements = new Elements(elems)
     def apply(elems: String*): Elements = apply(Set(elems: _*))
     val empty: Elements = apply()
     val full: Elements =
       new Elements(Set.empty)
       {
         override def apply(elem: String): Boolean = true
         override def toString: String = "Elements.full"
       }
   }
 
   sealed class Elements private[Markup](private val rep: Set[String])
   {
     def apply(elem: String): Boolean = rep.contains(elem)
     def + (elem: String): Elements = new Elements(rep + elem)
     def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     def - (elem: String): Elements = new Elements(rep - elem)
     def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     override def toString: String = rep.mkString("Elements(", ",", ")")
   }
 
 
   /* properties */
 
   val NAME = "name"
   val Name = new Properties.String(NAME)
 
   val XNAME = "xname"
   val XName = new Properties.String(XNAME)
 
   val KIND = "kind"
   val Kind = new Properties.String(KIND)
 
   val CONTENT = "content"
   val Content = new Properties.String(CONTENT)
 
   val SERIAL = "serial"
   val Serial = new Properties.Long(SERIAL)
 
   val INSTANCE = "instance"
   val Instance = new Properties.String(INSTANCE)
 
 
   /* basic markup */
 
   val Empty: Markup = Markup("", Nil)
   val Broken: Markup = Markup("broken", Nil)
 
   class Markup_String(val name: String, prop: String)
   {
     private val Prop = new Properties.String(prop)
 
     def apply(s: String): Markup = Markup(name, Prop(s))
     def unapply(markup: Markup): Option[String] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
   class Markup_Int(val name: String, prop: String)
   {
     private val Prop = new Properties.Int(prop)
 
     def apply(i: Int): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
   class Markup_Long(val name: String, prop: String)
   {
     private val Prop = new Properties.Long(prop)
 
     def apply(i: Long): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Long] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
 
   /* meta data */
 
   val META_TITLE = "meta_title"
   val META_CREATOR = "meta_creator"
   val META_CONTRIBUTOR = "meta_contributor"
   val META_DATE = "meta_date"
   val META_LICENSE = "meta_license"
   val META_DESCRIPTION = "meta_description"
 
 
   /* formal entities */
 
   val BINDING = "binding"
   val ENTITY = "entity"
 
   object Entity
   {
     val Def = new Properties.Long("def")
     val Ref = new Properties.Long("ref")
 
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) =>
           val kind = Kind.unapply(props).getOrElse("")
           val name = Name.unapply(props).getOrElse("")
           Some((kind, name))
         case _ => None
       }
   }
 
 
   /* completion */
 
   val COMPLETION = "completion"
   val NO_COMPLETION = "no_completion"
 
   val UPDATE = "update"
 
 
   /* position */
 
   val LINE = "line"
   val END_LINE = "line"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   val POSITION = "position"
 
 
   /* expression */
 
   val EXPRESSION = "expression"
   object Expression
   {
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(EXPRESSION, Kind(kind)) => Some(kind)
         case Markup(EXPRESSION, _) => Some("")
         case _ => None
       }
   }
 
 
   /* citation */
 
   val CITATION = "citation"
   val Citation = new Markup_String(CITATION, NAME)
 
 
   /* embedded languages */
 
   val Symbols = new Properties.Boolean("symbols")
   val Antiquotes = new Properties.Boolean("antiquotes")
   val Delimited = new Properties.Boolean("delimited")
 
   val LANGUAGE = "language"
   object Language
   {
     val DOCUMENT = "document"
     val ML = "ML"
     val SML = "SML"
     val PATH = "path"
     val UNKNOWN = "unknown"
 
     def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
       markup match {
         case Markup(LANGUAGE, props) =>
           (props, props, props, props) match {
             case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
               Some((name, symbols, antiquotes, delimited))
             case _ => None
           }
         case _ => None
       }
   }
 
 
   /* external resources */
 
   val PATH = "path"
   val Path = new Markup_String(PATH, NAME)
 
   val EXPORT_PATH = "export_path"
   val Export_Path = new Markup_String(EXPORT_PATH, NAME)
 
   val URL = "url"
   val Url = new Markup_String(URL, NAME)
 
   val DOC = "doc"
   val Doc = new Markup_String(DOC, NAME)
 
 
   /* pretty printing */
 
   val Consistent = new Properties.Boolean("consistent")
   val Indent = new Properties.Int("indent")
   val Width = new Properties.Int("width")
 
   object Block
   {
     val name = "block"
     def apply(c: Boolean, i: Int): Markup =
       Markup(name,
         (if (c) Consistent(c) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Boolean, Int)] =
       if (markup.name == name) {
         val c = Consistent.unapply(markup.properties).getOrElse(false)
         val i = Indent.unapply(markup.properties).getOrElse(0)
         Some((c, i))
       }
       else None
   }
 
   object Break
   {
     val name = "break"
     def apply(w: Int, i: Int): Markup =
       Markup(name,
         (if (w != 0) Width(w) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Int, Int)] =
       if (markup.name == name) {
         val w = Width.unapply(markup.properties).getOrElse(0)
         val i = Indent.unapply(markup.properties).getOrElse(0)
         Some((w, i))
       }
       else None
   }
 
   val ITEM = "item"
   val BULLET = "bullet"
 
   val SEPARATOR = "separator"
 
 
   /* text properties */
 
   val WORDS = "words"
 
   val HIDDEN = "hidden"
 
   val DELETE = "delete"
 
 
   /* misc entities */
 
   val CLASS = "class"
   val TYPE_NAME = "type_name"
   val FIXED = "fixed"
   val CASE = "case"
   val CONSTANT = "constant"
   val DYNAMIC_FACT = "dynamic_fact"
 
 
   /* inner syntax */
 
   val TFREE = "tfree"
   val TVAR = "tvar"
   val FREE = "free"
   val SKOLEM = "skolem"
   val BOUND = "bound"
   val VAR = "var"
   val NUMERAL = "numeral"
   val LITERAL = "literal"
   val DELIMITER = "delimiter"
   val INNER_STRING = "inner_string"
   val INNER_CARTOUCHE = "inner_cartouche"
 
   val TOKEN_RANGE = "token_range"
 
   val SORTING = "sorting"
   val TYPING = "typing"
   val CLASS_PARAMETER = "class_parameter"
 
   val ATTRIBUTE = "attribute"
   val METHOD = "method"
 
 
   /* antiquotations */
 
   val ANTIQUOTED = "antiquoted"
   val ANTIQUOTE = "antiquote"
 
   val ML_ANTIQUOTATION = "ML_antiquotation"
   val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
   /* document text */
 
   val RAW_TEXT = "raw_text"
   val PLAIN_TEXT = "plain_text"
 
   val PARAGRAPH = "paragraph"
   val TEXT_FOLD = "text_fold"
 
   object Document_Tag
   {
     val ELEMENT = "document_tag"
     val IMPORTANT = "important"
     val UNIMPORTANT = "unimportant"
 
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(ELEMENT, Name(name)) => Some(name)
         case _ => None
       }
   }
 
 
   /* Markdown document structure */
 
   val MARKDOWN_PARAGRAPH = "markdown_paragraph"
   val MARKDOWN_ITEM = "markdown_item"
   val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
   val Markdown_List = new Markup_String("markdown_list", "kind")
 
   val ITEMIZE = "itemize"
   val ENUMERATE = "enumerate"
   val DESCRIPTION = "description"
 
 
   /* ML */
 
   val ML_KEYWORD1 = "ML_keyword1"
   val ML_KEYWORD2 = "ML_keyword2"
   val ML_KEYWORD3 = "ML_keyword3"
   val ML_DELIMITER = "ML_delimiter"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
   val ML_COMMENT = "ML_comment"
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
   val ML_STRUCTURE = "ML_structure"
   val ML_TYPING = "ML_typing"
 
   val ML_BREAKPOINT = "ML_breakpoint"
 
 
   /* outer syntax */
 
   val COMMAND = "command"
   val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"
   val KEYWORD2 = "keyword2"
   val KEYWORD3 = "keyword3"
   val QUASI_KEYWORD = "quasi_keyword"
   val IMPROPER = "improper"
   val OPERATOR = "operator"
   val STRING = "string"
   val ALT_STRING = "alt_string"
   val VERBATIM = "verbatim"
   val CARTOUCHE = "cartouche"
   val COMMENT = "comment"
 
 
   /* comments */
 
   val COMMENT1 = "comment1"
   val COMMENT2 = "comment2"
   val COMMENT3 = "comment3"
 
 
   /* timing */
 
   val Elapsed = new Properties.Double("elapsed")
   val CPU = new Properties.Double("cpu")
   val GC = new Properties.Double("gc")
 
   object Timing_Properties
   {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
 
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {
         case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
           Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
         case _ => None
       }
   }
 
   val TIMING = "timing"
 
   object Timing
   {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
 
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
         case _ => None
       }
   }
 
 
   /* process result */
 
   val Return_Code = new Properties.Int("return_code")
 
   object Process_Result
   {
     def apply(result: Process_Result): Properties.T =
       Return_Code(result.rc) :::
         (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
 
     def unapply(props: Properties.T): Option[Process_Result] =
       props match {
         case Return_Code(rc) =>
           val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
           Some(isabelle.Process_Result(rc, timing = timing))
         case _ => None
       }
   }
 
 
   /* command indentation */
 
   object Command_Indent
   {
     val name = "command_indent"
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Indent.unapply(markup.properties) else None
   }
 
 
   /* goals */
 
   val GOAL = "goal"
   val SUBGOAL = "subgoal"
 
 
   /* command status */
 
   val TASK = "task"
 
   val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
   val CANCELED = "canceled"
   val INITIALIZED = "initialized"
   val FINALIZED = "finalized"
   val CONSOLIDATING = "consolidating"
   val CONSOLIDATED = "consolidated"
 
 
   /* interactive documents */
 
   val VERSION = "version"
   val ASSIGN = "assign"
 
 
   /* prover process */
 
   val PROVER_COMMAND = "prover_command"
   val PROVER_ARG = "prover_arg"
 
 
   /* messages */
 
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"
   val RESULT = "result"
   val WRITELN = "writeln"
   val STATE = "state"
   val INFORMATION = "information"
   val TRACING = "tracing"
   val WARNING = "warning"
   val LEGACY = "legacy"
   val ERROR = "error"
   val NODES_STATUS = "nodes_status"
   val PROTOCOL = "protocol"
   val SYSTEM = "system"
   val STDOUT = "stdout"
   val STDERR = "stderr"
   val EXIT = "exit"
 
   val WRITELN_MESSAGE = "writeln_message"
   val STATE_MESSAGE = "state_message"
   val INFORMATION_MESSAGE = "information_message"
   val TRACING_MESSAGE = "tracing_message"
   val WARNING_MESSAGE = "warning_message"
   val LEGACY_MESSAGE = "legacy_message"
   val ERROR_MESSAGE = "error_message"
 
   val messages = Map(
     WRITELN -> WRITELN_MESSAGE,
     STATE -> STATE_MESSAGE,
     INFORMATION -> INFORMATION_MESSAGE,
     TRACING -> TRACING_MESSAGE,
     WARNING -> WARNING_MESSAGE,
     LEGACY -> LEGACY_MESSAGE,
     ERROR -> ERROR_MESSAGE)
 
   val message: String => String = messages.withDefault((s: String) => s)
 
   val NO_REPORT = "no_report"
 
   val BAD = "bad"
 
   val INTENSIFY = "intensify"
 
 
   /* active areas */
 
   val BROWSER = "browser"
   val GRAPHVIEW = "graphview"
   val THEORY_EXPORTS = "theory_exports"
 
   val SENDBACK = "sendback"
   val PADDING = "padding"
   val PADDING_LINE = (PADDING, "line")
   val PADDING_COMMAND = (PADDING, "command")
 
   val DIALOG = "dialog"
   val Result = new Properties.String(RESULT)
 
   val JEDIT_ACTION = "jedit_action"
 
 
   /* protocol message functions */
 
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)
 
   val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
   val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
 
   val Commands_Accepted: Properties.T = List((FUNCTION, "commands_accepted"))
   val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 
   object Protocol_Handler
   {
     def unapply(props: Properties.T): Option[(String)] =
       props match {
         case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
   val INVOKE_SCALA = "invoke_scala"
   object Invoke_Scala
   {
     def unapply(props: Properties.T): Option[(String, String)] =
       props match {
         case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
 
   val CANCEL_SCALA = "cancel_scala"
   object Cancel_Scala
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
         case _ => None
       }
   }
 
   object ML_Statistics
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
         case (FUNCTION, "ML_statistics") :: props => Some(props)
         case _ => None
       }
   }
 
   object Task_Statistics
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
         case (FUNCTION, "task_statistics") :: props => Some(props)
         case _ => None
       }
   }
 
   val LOADING_THEORY = "loading_theory"
   object Loading_Theory
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
   val BUILD_SESSION_FINISHED = "build_session_finished"
   val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
 
   val PRINT_OPERATIONS = "print_operations"
 
 
 
   /* export */
 
   val EXPORT = "export"
-  val Export_Marker = Protocol_Message.Marker(EXPORT)
-
-  object Export
-  {
-    sealed case class Args(
-      id: Option[String],
-      serial: Long,
-      theory_name: String,
-      name: String,
-      executable: Boolean,
-      compress: Boolean,
-      strict: Boolean)
-    {
-      def compound_name: String = isabelle.Export.compound_name(theory_name, name)
-    }
-
-    val THEORY_NAME = "theory_name"
-    val EXECUTABLE = "executable"
-    val COMPRESS = "compress"
-    val STRICT = "strict"
-
-    object Marker
-    {
-      def unapply(line: String): Option[(Args, Path)] =
-        line match {
-          case Export_Marker(text) =>
-            val props = XML.Decode.properties(YXML.parse_body(text))
-            props match {
-              case
-                List(
-                  (SERIAL, Value.Long(serial)),
-                  (THEORY_NAME, theory_name),
-                  (NAME, name),
-                  (EXECUTABLE, Value.Boolean(executable)),
-                  (COMPRESS, Value.Boolean(compress)),
-                  (STRICT, Value.Boolean(strict)),
-                  (FILE, file)) if isabelle.Path.is_valid(file) =>
-                val args = Args(None, serial, theory_name, name, executable, compress, strict)
-                Some((args, isabelle.Path.explode(file)))
-              case _ => None
-            }
-          case _ => None
-        }
-    }
-
-    def unapply(props: Properties.T): Option[Args] =
-      props match {
-        case
-          List(
-            (FUNCTION, EXPORT),
-            (ID, id),
-            (SERIAL, Value.Long(serial)),
-            (THEORY_NAME, theory_name),
-            (NAME, name),
-            (EXECUTABLE, Value.Boolean(executable)),
-            (COMPRESS, Value.Boolean(compress)),
-            (STRICT, Value.Boolean(strict))) =>
-          Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict))
-        case _ => None
-      }
-  }
+  val THEORY_NAME = "theory_name"
+  val EXECUTABLE = "executable"
+  val COMPRESS = "compress"
+  val STRICT = "strict"
 
 
   /* debugger output */
 
   val DEBUGGER_STATE = "debugger_state"
   object Debugger_State
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
   val DEBUGGER_OUTPUT = "debugger_output"
   object Debugger_Output
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
 
   /* simplifier trace */
 
   val SIMP_TRACE_PANEL = "simp_trace_panel"
 
   val SIMP_TRACE_LOG = "simp_trace_log"
   val SIMP_TRACE_STEP = "simp_trace_step"
   val SIMP_TRACE_RECURSE = "simp_trace_recurse"
   val SIMP_TRACE_HINT = "simp_trace_hint"
   val SIMP_TRACE_IGNORE = "simp_trace_ignore"
 
   val SIMP_TRACE_CANCEL = "simp_trace_cancel"
   object Simp_Trace_Cancel
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
         case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
         case _ => None
       }
   }
 
 
   /* XML data representation */
 
   def encode: XML.Encode.T[Markup] = (markup: Markup) =>
   {
     import XML.Encode._
     pair(string, properties)((markup.name, markup.properties))
   }
 
   def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
   {
     import XML.Decode._
     val (name, props) = pair(string, properties)(body)
     Markup(name, props)
   }
 }
 
 
 sealed case class Markup(name: String, properties: Properties.T)
 {
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
 
   def update_properties(more_props: Properties.T): Markup =
     if (more_props.isEmpty) this
     else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
 
   def + (entry: Properties.Entry): Markup =
     Markup(name, Properties.put(properties, entry))
 }
diff --git a/src/Pure/PIDE/protocol.scala b/src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala
+++ b/src/Pure/PIDE/protocol.scala
@@ -1,381 +1,441 @@
 /*  Title:      Pure/PIDE/protocol.scala
     Author:     Makarius
 
 Protocol message formats for interactive proof documents.
 */
 
 package isabelle
 
 
 object Protocol
 {
   /* document editing */
 
   object Commands_Accepted
   {
     def unapply(text: String): Option[List[Document_ID.Command]] =
       try { Some(space_explode(',', text).map(Value.Long.parse)) }
       catch { case ERROR(_) => None }
 
     val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED)))
   }
 
   object Assign_Update
   {
     def unapply(text: String)
       : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
     {
       try {
         import XML.Decode._
         def decode_upd(body: XML.Body): (Long, List[Long]) =
           space_explode(',', string(body)).map(Value.Long.parse) match {
             case a :: bs => (a, bs)
             case _ => throw new XML.XML_Body(body)
           }
         Some(triple(long, list(string), list(decode_upd))(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
         case _: XML.Error => None
       }
     }
   }
 
   object Removed
   {
     def unapply(text: String): Option[List[Document_ID.Version]] =
       try {
         import XML.Decode._
         Some(list(long)(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
         case _: XML.Error => None
       }
   }
 
 
   /* command timing */
 
   object Command_Timing
   {
     def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
       props match {
         case Markup.COMMAND_TIMING :: args =>
           (args, args) match {
             case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
             case _ => None
           }
         case _ => None
       }
   }
 
 
   /* theory timing */
 
   object Theory_Timing
   {
     def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
       props match {
         case Markup.THEORY_TIMING :: args =>
           (args, args) match {
             case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
             case _ => None
           }
         case _ => None
       }
   }
 
 
   /* result messages */
 
   def is_result(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.RESULT, _), _) => true
       case _ => false
     }
 
   def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.TRACING, _), _) => true
       case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_state(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.STATE, _), _) => true
       case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_information(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
       case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_writeln(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WRITELN, _), _) => true
       case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true
       case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_legacy(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.LEGACY, _), _) => true
       case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_error(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.ERROR, _), _) => true
       case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_inlined(msg: XML.Tree): Boolean =
     !(is_result(msg) || is_tracing(msg) || is_state(msg))
 
   def is_exported(msg: XML.Tree): Boolean =
     is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
 
   def message_text(msg: XML.Tree): String =
   {
     val text = Pretty.string_of(List(msg))
     if (is_warning(msg) || is_legacy(msg)) Library.prefix_lines("### ", text)
     else if (is_error(msg)) Library.prefix_lines("*** ", text)
     else text
   }
 
 
+  /* export */
+
+  val Export_Marker = Protocol_Message.Marker(Markup.EXPORT)
+
+  object Export
+  {
+    sealed case class Args(
+      id: Option[String],
+      serial: Long,
+      theory_name: String,
+      name: String,
+      executable: Boolean,
+      compress: Boolean,
+      strict: Boolean)
+    {
+      def compound_name: String = isabelle.Export.compound_name(theory_name, name)
+    }
+
+    object Marker
+    {
+      def unapply(line: String): Option[(Args, Path)] =
+        line match {
+          case Export_Marker(text) =>
+            val props = XML.Decode.properties(YXML.parse_body(text))
+            props match {
+              case
+                List(
+                  (Markup.SERIAL, Value.Long(serial)),
+                  (Markup.THEORY_NAME, theory_name),
+                  (Markup.NAME, name),
+                  (Markup.EXECUTABLE, Value.Boolean(executable)),
+                  (Markup.COMPRESS, Value.Boolean(compress)),
+                  (Markup.STRICT, Value.Boolean(strict)),
+                  (Markup.FILE, file)) if isabelle.Path.is_valid(file) =>
+                val args = Args(None, serial, theory_name, name, executable, compress, strict)
+                Some((args, isabelle.Path.explode(file)))
+              case _ => None
+            }
+          case _ => None
+        }
+    }
+
+    def unapply(props: Properties.T): Option[Args] =
+      props match {
+        case
+          List(
+            (Markup.FUNCTION, Markup.EXPORT),
+            (Markup.ID, id),
+            (Markup.SERIAL, Value.Long(serial)),
+            (Markup.THEORY_NAME, theory_name),
+            (Markup.NAME, name),
+            (Markup.EXECUTABLE, Value.Boolean(executable)),
+            (Markup.COMPRESS, Value.Boolean(compress)),
+            (Markup.STRICT, Value.Boolean(strict))) =>
+          Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict))
+        case _ => None
+      }
+  }
+
+
   /* breakpoints */
 
   object ML_Breakpoint
   {
     def unapply(tree: XML.Tree): Option[Long] =
     tree match {
       case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
       case _ => None
     }
   }
 
 
   /* dialogs */
 
   object Dialog_Args
   {
     def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
       (props, props, props) match {
         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
           Some((id, serial, result))
         case _ => None
       }
   }
 
   object Dialog
   {
     def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
       tree match {
         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
           Some((id, serial, result))
         case _ => None
       }
   }
 
   object Dialog_Result
   {
     def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
     {
       val props = Position.Id(id) ::: Markup.Serial(serial)
       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
     }
 
     def unapply(tree: XML.Tree): Option[String] =
       tree match {
         case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
         case _ => None
       }
   }
 }
 
 
 trait Protocol
 {
   /* protocol commands */
 
   def protocol_command_raw(name: String, args: List[Bytes]): Unit
   def protocol_command_args(name: String, args: List[String])
   def protocol_command(name: String, args: String*): Unit
 
 
   /* options */
 
   def options(opts: Options): Unit =
     protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
 
 
   /* session base */
 
   private def encode_table(table: List[(String, String)]): String =
   {
     import XML.Encode._
     Symbol.encode_yxml(list(pair(string, string))(table))
   }
 
   private def encode_list(lst: List[String]): String =
   {
     import XML.Encode._
     Symbol.encode_yxml(list(string)(lst))
   }
 
   private def encode_sessions(lst: List[(String, Position.T)]): String =
   {
     import XML.Encode._
     Symbol.encode_yxml(list(pair(string, properties))(lst))
   }
 
   def session_base(resources: Resources)
   {
     protocol_command("Prover.init_session_base",
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),
       encode_list(resources.session_base.doc_names),
       encode_table(resources.session_base.global_theories.toList),
       encode_list(resources.session_base.loaded_theories.keys))
   }
 
 
   /* interned items */
 
   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes))
 
   private def encode_command(command: Command): (String, String, String, String, List[String]) =
   {
     import XML.Encode._
 
     val blobs_yxml =
     {
       val encode_blob: T[Command.Blob] =
         variant(List(
           { case Exn.Res((a, b)) =>
               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
 
       Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     }
 
     val toks_yxml =
     {
       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
       Symbol.encode_yxml(list(encode_tok)(command.span.content))
     }
     val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source))
 
     (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources)
   }
 
   def define_command(command: Command)
   {
     val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command)
     protocol_command_args(
       "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources)
   }
 
   def define_commands(commands: List[Command])
   {
     protocol_command_args("Document.define_commands",
       commands.map(command =>
       {
         import XML.Encode._
         val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command)
         val body =
           pair(string, pair(string, pair(string, pair(string, list(string)))))(
             command_id, (name, (blobs_yxml, (toks_yxml, toks_sources))))
         YXML.string_of_body(body)
       }))
   }
 
   def define_commands_bulk(commands: List[Command])
   {
     val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
     irregular.foreach(define_command)
     regular match {
       case Nil =>
       case List(command) => define_command(command)
       case _ => define_commands(regular)
     }
   }
 
 
   /* execution */
 
   def discontinue_execution(): Unit =
     protocol_command("Document.discontinue_execution")
 
   def cancel_exec(id: Document_ID.Exec): Unit =
     protocol_command("Document.cancel_exec", Document_ID(id))
 
 
   /* document versions */
 
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
   {
     val consolidate_yxml =
     {
       import XML.Encode._
       Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
     }
     val edits_yxml =
     {
       import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
         variant(List(
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val master_dir = File.standard_url(name.master_dir)
               val imports = header.imports.map(_.node)
               val keywords =
                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
               (Nil,
                 pair(string, pair(string, pair(list(string), pair(list(pair(string,
                     pair(pair(string, list(string)), list(string)))), list(string)))))(
                 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(string, list(string))))(c.dest)) }))
       edits.map({ case (name, edit) =>
         Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) })
     }
     protocol_command_args("Document.update",
       Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml)
   }
 
   def remove_versions(versions: List[Document.Version])
   {
     val versions_yxml =
     { import XML.Encode._
       Symbol.encode_yxml(list(long)(versions.map(_.id))) }
     protocol_command("Document.remove_versions", versions_yxml)
   }
 
 
   /* dialog via document content */
 
   def dialog_result(serial: Long, result: String): Unit =
     protocol_command("Document.dialog_result", Value.Long(serial), result)
 }
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,746 +1,746 @@
 /*  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 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 */
 
   abstract class Protocol_Handler
   {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
     val functions: List[(String, Prover.Protocol_Output => Boolean)]
   }
 }
 
 
 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 statistics = new Session.Outlet[Session.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 = Standard_Thread.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 =
       Standard_Thread.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 =
     resources.file_formats.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 =
     Standard_Thread.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(state_id, timing) if prover.defined =>
                 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 Protocol.Theory_Timing(_, _) =>
                 // FIXME
 
-              case Markup.Export(args)
+              case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 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 Markup.Commands_Accepted =>
                 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 Markup.Assign_Update =>
                 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 Markup.Removed_Versions =>
                 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 Markup.ML_Statistics(props) =>
                 statistics.post(Session.Statistics(props))
 
               case Markup.Task_Statistics(props) =>
                 // FIXME
 
               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.session_base(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) {
       Thread.sleep(output_delay.ms)
       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 send_stop()
   {
     val was_ready =
       _phase.guarded_access(phase =>
         phase match {
           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)
   }
 
   def stop(): Process_Result =
   {
     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/export.scala b/src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala
+++ b/src/Pure/Thy/export.scala
@@ -1,419 +1,419 @@
 /*  Title:      Pure/Thy/export.scala
     Author:     Makarius
 
 Manage theory exports: compressed blobs.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.util.matching.Regex
 
 
 object Export
 {
   /* name structure */
 
   def explode_name(s: String): List[String] = space_explode('/', s)
   def implode_name(elems: Iterable[String]): String = elems.mkString("/")
 
 
   /* SQL data model */
 
   object Data
   {
     val session_name = SQL.Column.string("session_name").make_primary_key
     val theory_name = SQL.Column.string("theory_name").make_primary_key
     val name = SQL.Column.string("name").make_primary_key
     val executable = SQL.Column.bool("executable")
     val compressed = SQL.Column.bool("compressed")
     val body = SQL.Column.bytes("body")
 
     val table =
       SQL.Table("isabelle_exports",
         List(session_name, theory_name, name, executable, compressed, body))
 
     def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
       "WHERE " + Data.session_name.equal(session_name) +
         (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
         (if (name == "") "" else " AND " + Data.name.equal(name))
   }
 
   def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
   {
     val select =
       Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name))
     db.using_statement(select)(stmt => stmt.execute_query().next())
   }
 
   def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
   {
     val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res => res.string(Data.name)).toList)
   }
 
   def read_theory_names(db: SQL.Database, session_name: String): List[String] =
   {
     val select =
       Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
   }
 
   def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] =
   {
     val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res =>
         (res.string(Data.theory_name), res.string(Data.name))).toList)
   }
 
   def message(msg: String, theory_name: String, name: String): String =
     msg + " " + quote(name) + " for theory " + quote(theory_name)
 
   def compound_name(a: String, b: String): String = a + ":" + b
 
   sealed case class Entry(
     session_name: String,
     theory_name: String,
     name: String,
     executable: Boolean,
     body: Future[(Boolean, Bytes)])
   {
     override def toString: String = name
 
     def compound_name: String = Export.compound_name(theory_name, name)
 
     val name_elems: List[String] = explode_name(name)
 
     def name_extends(elems: List[String]): Boolean =
       name_elems.startsWith(elems) && name_elems != elems
 
     def text: String = uncompressed().text
 
     def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
     {
       val (compressed, bytes) = body.join
       if (compressed) bytes.uncompress(cache = cache) else bytes
     }
 
     def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
       YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
 
     def write(db: SQL.Database)
     {
       val (compressed, bytes) = body.join
       db.using_statement(Data.table.insert())(stmt =>
       {
         stmt.string(1) = session_name
         stmt.string(2) = theory_name
         stmt.string(3) = name
         stmt.bool(4) = executable
         stmt.bool(5) = compressed
         stmt.bytes(6) = bytes
         stmt.execute()
       })
     }
   }
 
   def make_regex(pattern: String): Regex =
   {
     @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
       chs match {
         case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
         case '*' :: rest => make("[^:/]*" :: result, depth, rest)
         case '?' :: rest => make("[^:/]" :: result, depth, rest)
         case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
         case '{' :: rest => make("(" :: result, depth + 1, rest)
         case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
         case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
         case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
         case c :: rest => make(c.toString :: result, depth, rest)
         case Nil => result.reverse.mkString.r
       }
     make(Nil, 0, pattern.toList)
   }
 
   def make_matcher(pattern: String): (String, String) => Boolean =
   {
     val regex = make_regex(pattern)
     (theory_name: String, name: String) =>
       regex.pattern.matcher(compound_name(theory_name, name)).matches
   }
 
-  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
+  def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes,
     cache: XZ.Cache = XZ.cache()): Entry =
   {
     Entry(session_name, args.theory_name, args.name, args.executable,
       if (args.compress) Future.fork(body.maybe_compress(cache = cache))
       else Future.value((false, body)))
   }
 
   def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String)
     : Option[Entry] =
   {
     val select =
       Data.table.select(List(Data.executable, Data.compressed, Data.body),
         Data.where_equal(session_name, theory_name, name))
     db.using_statement(select)(stmt =>
     {
       val res = stmt.execute_query()
       if (res.next()) {
         val executable = res.bool(Data.executable)
         val compressed = res.bool(Data.compressed)
         val body = res.bytes(Data.body)
         Some(Entry(session_name, theory_name, name, executable, Future.value(compressed, body)))
       }
       else None
     })
   }
 
   def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] =
   {
     val path = dir + Path.basic(theory_name) + Path.explode(name)
     if (path.is_file) {
       val executable = File.is_executable(path)
       val uncompressed = Bytes.read(path)
       Some(Entry(session_name, theory_name, name, executable, Future.value((false, uncompressed))))
     }
     else None
   }
 
 
   /* database consumer thread */
 
   def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
 
   class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
   {
     private val errors = Synchronized[List[String]](Nil)
 
     private val consumer =
       Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
         bulk = { case (entry, _) => entry.body.is_finished },
         consume =
           (args: List[(Entry, Boolean)]) =>
           {
             val results =
               db.transaction {
                 for ((entry, strict) <- args)
                 yield {
                   if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
                     if (strict) {
                       val msg = message("Duplicate export", entry.theory_name, entry.name)
                       errors.change(msg :: _)
                     }
                     Exn.Res(())
                   }
                   else Exn.capture { entry.write(db) }
                 }
               }
             (results, true)
           })
 
-    def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
+    def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit =
       consumer.send(make_entry(session_name, args, body, cache = cache) -> args.strict)
 
     def shutdown(close: Boolean = false): List[String] =
     {
       consumer.shutdown()
       if (close) db.close()
       errors.value.reverse
     }
   }
 
 
   /* abstract provider */
 
   object Provider
   {
     def none: Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] = None
         def focus(other_theory: String): Provider = this
 
         override def toString: String = "none"
       }
 
     def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
           read_entry(db, session_name, theory_name, export_name)
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory_name) this
           else Provider.database(db, session_name, other_theory)
 
         override def toString: String = db.toString
       }
 
     def snapshot(snapshot: Document.Snapshot): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
           snapshot.exports_map.get(export_name)
 
         def focus(other_theory: String): Provider =
           if (other_theory == snapshot.node_name.theory) this
           else {
             val node_name =
               snapshot.version.nodes.theory_name(other_theory) getOrElse
                 error("Bad theory " + quote(other_theory))
             Provider.snapshot(snapshot.state.snapshot(node_name))
           }
 
         override def toString: String = snapshot.toString
       }
 
     def directory(dir: Path, session_name: String, theory_name: String): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
           read_entry(dir, session_name, theory_name, export_name)
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory_name) this
           else Provider.directory(dir, session_name, other_theory)
 
         override def toString: String = dir.toString
       }
   }
 
   trait Provider
   {
     def apply(export_name: String): Option[Entry]
 
     def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body =
       apply(export_name) match {
         case Some(entry) => entry.uncompressed_yxml(cache = cache)
         case None => Nil
       }
 
     def focus(other_theory: String): Provider
   }
 
 
   /* export to file-system */
 
   def export_files(
     store: Sessions.Store,
     session_name: String,
     export_dir: Path,
     progress: Progress = No_Progress,
     export_prune: Int = 0,
     export_list: Boolean = false,
     export_patterns: List[String] = Nil)
   {
     using(store.open_database(session_name))(db =>
     {
       db.transaction {
         val export_names = read_theory_exports(db, session_name)
 
         // list
         if (export_list) {
           (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
             sorted.foreach(progress.echo)
         }
 
         // export
         if (export_patterns.nonEmpty) {
           val exports =
             (for {
               export_pattern <- export_patterns.iterator
               matcher = make_matcher(export_pattern)
               (theory_name, name) <- export_names if matcher(theory_name, name)
             } yield (theory_name, name)).toSet
           for {
             (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
             name <- group.map(_._2).sorted
             entry <- read_entry(db, session_name, theory_name, name)
           } {
             val elems = theory_name :: space_explode('/', name)
             val path =
               if (elems.length < export_prune + 1) {
                 error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))
               }
               else export_dir + Path.make(elems.drop(export_prune))
 
             progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
             Isabelle_System.mkdirs(path.dir)
             Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
             File.set_executable(path, entry.executable)
           }
         }
       }
     })
   }
 
 
   /* Isabelle tool wrapper */
 
   val default_export_dir: Path = Path.explode("export")
 
   val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
   {
     /* arguments */
 
     var export_dir = default_export_dir
     var dirs: List[Path] = Nil
     var export_list = false
     var no_build = false
     var options = Options.init()
     var export_prune = 0
     var export_patterns: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle export [OPTIONS] SESSION
 
   Options are:
     -O DIR       output directory for exported files (default: """ + default_export_dir + """)
     -d DIR       include session directory
     -l           list exports
     -n           no build of session
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NUM       prune path of exported files by NUM elements
     -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
 
   List or export theory exports for SESSION: named blobs produced by
   isabelle build. Option -l or -x is required; option -x may be repeated.
 
   The PATTERN language resembles glob patterns in the shell, with ? and *
   (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
   and variants {pattern1,pattern2,pattern3}.
 """,
       "O:" -> (arg => export_dir = Path.explode(arg)),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "l" -> (_ => export_list = true),
       "n" -> (_ => no_build = true),
       "o:" -> (arg => options = options + arg),
       "p:" -> (arg => export_prune = Value.Int.parse(arg)),
       "x:" -> (arg => export_patterns ::= arg))
 
     val more_args = getopts(args)
     val session_name =
       more_args match {
         case List(session_name) if export_list || export_patterns.nonEmpty => session_name
         case _ => getopts.usage()
       }
 
     val progress = new Console_Progress()
 
 
     /* build */
 
     if (!no_build) {
       val rc =
         progress.interrupt_handler {
           Build.build_logic(options, session_name, progress = progress, dirs = dirs)
         }
       if (rc != 0) sys.exit(rc)
     }
 
 
     /* export files */
 
     val store = Sessions.store(options)
     export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
       export_list = export_list, export_patterns = export_patterns)
   })
 }
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,872 +1,872 @@
 /*  Title:      Pure/Tools/build.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Build and manage Isabelle sessions.
 */
 
 package isabelle
 
 
 import scala.collection.SortedSet
 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, name: String): Timings =
     {
       val no_timings: Timings = (Nil, 0.0)
 
       store.access_database(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, name)
             val session_timing =
               store.read_session_timing(db, 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(name: String): Double =
       {
         if (maximals.contains(name)) timing(name)
         else {
           val descendants = sessions_structure.build_descendants(List(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.get(p).isEmpty)) 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 */
 
   class Handler(progress: Progress, session: Session, session_name: String)
     extends Session.Protocol_Handler
   {
     val result_error: Promise[String] = Future.promise
 
     override def exit() { result_error.cancel }
 
     private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
     {
       val error_message =
         try { Pretty.string_of(Symbol.decode_yxml(msg.text)) }
         catch { case ERROR(msg) => msg }
       result_error.fulfill(error_message)
       session.send_stop()
       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
       }
 
     val functions =
       List(
         Markup.BUILD_SESSION_FINISHED -> build_session_finished,
         Markup.LOADING_THEORY -> loading_theory)
   }
 
 
   /* job: running prover process */
 
   private val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
 
   private class Job(progress: Progress,
     name: String,
     val info: Sessions.Info,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_store: Boolean,
     verbose: Boolean,
     pide: Boolean,
     val numa_node: Option[Int],
     command_timings: List[Properties.T])
   {
     private val 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")
     isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
 
     private val export_tmp_dir = Isabelle_System.tmp_dir("export")
     private val export_consumer =
       Export.consumer(store.open_database(name, output = true), cache = store.xz_cache)
 
     private val future_result: Future[Process_Result] =
       Future.thread("build") {
         val parent = info.parent.getOrElse("")
         val base = deps(name)
         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, (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(name)
 
         val eval_store =
           if (!do_store) Nil
           else {
             (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(name))))
           }
 
         if (pide && !is_pure) {
           val resources = new Resources(sessions_structure, deps(parent))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
 
           val process =
             Isabelle_Process(session, options, sessions_structure, store,
               logic = parent, cwd = info.dir.file, env = env).await_startup
 
           session.protocol_command("build_session", args_yxml)
 
           val result = process.join
           handler.result_error.join match {
             case "" => result
             case msg =>
               result.copy(
                 rc = result.rc max 1,
                 out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
           }
         }
         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 = Command_Line.ML_tool0(eval_build :: eval_store)
 
           val process =
             if (is_pure) {
               ML_Process(options, deps.sessions_structure, store, raw_ml_system = true,
                 args =
                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
                     List("--eval", eval),
                 cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
             }
             else {
               ML_Process(options, deps.sessions_structure, store, logic = parent,
                 args = List("--eval", eval),
                 cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
             }
 
           process.result(
             progress_stdout = (line: String) =>
               line match {
                 case Loading_Theory_Marker(theory) =>
                   progress.theory(Progress.Theory(theory, session = name))
-                case Markup.Export.Marker((args, path)) =>
+                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(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, 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(name).is_file)
           Some(Sessions.write_heap_digest(store.output_heap(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,
     progress: Progress = No_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,
     pide: Boolean = false,
     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,
     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   {
     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
 
     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, name: String): String =
     {
       val digests =
         full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
     }
 
     val selection1 =
       Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
         exclude_sessions, session_groups, sessions) ++ selection
 
     val deps =
     {
       val deps0 =
         Sessions.deps(full_sessions.selection(selection1),
           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(selection1))) {
         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()
     {
       try { Thread.sleep(500) }
       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
     }
 
     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((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(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(name), terminate_lines(log_lines))
             }
             else File.write(store.output_log(name), terminate_lines(log_lines))
 
             // write database
             {
               val build_log =
                 Build_Log.Log_File(name, process_result.out_lines).
                   parse_session_info(
                     command_timings = true,
                     theory_timings = true,
                     ml_statistics = true,
                     task_statistics = true)
 
               using(store.open_database(name, output = true))(db =>
                 store.write_session_info(db, name,
                   build_log =
                     if (process_result.timeout) build_log.error("Timeout") else build_log,
                   build =
                     Session_Info(sources_stamp(deps, name), input_heaps, heap_digest,
                       process_result.rc)))
             }
 
             // messages
             process_result.err_lines.foreach(progress.echo)
 
             if (process_result.ok)
               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
             else {
               progress.echo(name + " FAILED")
               if (!process_result.interrupted) progress.echo(process_result_tail.out)
             }
 
             loop(pending - name, running - name,
               results + (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((name, info)) =>
                 val ancestor_results =
                   deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
                     map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
 
                 val do_store = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
 
                 val (current, heap_digest) =
                 {
                   store.access_database(name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, name)) match {
                         case Some(build) =>
                           val heap_digest = store.find_heap_digest(name)
                           val current =
                             !fresh_build &&
                             build.ok &&
                             build.sources == sources_stamp(deps, 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 - name, running,
                     results + (name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
                 else if (no_build) {
                   if (verbose) progress.echo("Skipping " + name + " ...")
                   loop(pending - name, running,
                     results + (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 ") + name + " ...")
 
                   store.clean_output(name)
                   using(store.open_database(name, output = true))(store.init_session_info(_, name))
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Job(progress, name, info, deps, store, do_store, verbose, pide = pide,
                       numa_node, queue.command_timings(name))
                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
                 }
                 else {
                   progress.echo(name + " CANCELLED")
                   loop(pending - name, running,
                     results + (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 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(selection1).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 No_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 pide = 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)
     -P           build via PIDE protocol
     -R           operate on 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),
       "P" -> (_ => pide = 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,
           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,
           pide = pide,
           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 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 = No_Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
     fresh: Boolean = false,
     strict: Boolean = false): Int =
   {
     val rc =
       if (!fresh && build(options, build_heap = build_heap, no_build = true, dirs = dirs,
           sessions = List(logic)).ok) 0
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
         Build.build(options, progress = progress, build_heap = build_heap, fresh_build = fresh,
           dirs = dirs, sessions = List(logic)).rc
       }
 
     if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
   }
 }