diff --git a/src/Pure/PIDE/markup.ML b/src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML
+++ b/src/Pure/PIDE/markup.ML
@@ -1,798 +1,801 @@
 (*  Title:      Pure/PIDE/markup.ML
     Author:     Makarius
 
 Quasi-abstract markup elements.
 *)
 
 signature MARKUP =
 sig
   type T = string * Properties.T
   val empty: T
   val is_empty: T -> bool
   val properties: Properties.T -> T -> T
   val nameN: string val name: string -> T -> T
   val xnameN: string val xname: string -> T -> T
   val kindN: string
   val serialN: string
   val serial_properties: int -> Properties.T
   val instanceN: string
   val meta_titleN: string val meta_title: T
   val meta_creatorN: string val meta_creator: T
   val meta_contributorN: string val meta_contributor: T
   val meta_dateN: string val meta_date: T
   val meta_licenseN: string val meta_license: T
   val meta_descriptionN: string val meta_description: T
   val languageN: string
   val symbolsN: string
   val delimitedN: string
   val is_delimited: Properties.T -> bool
   val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
   val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
   val language_Isar: bool -> T
   val language_method: T
   val language_attribute: T
   val language_sort: bool -> T
   val language_type: bool -> T
   val language_term: bool -> T
   val language_prop: bool -> T
   val language_ML: bool -> T
   val language_SML: bool -> T
   val language_document: bool -> T
   val language_document_marker: T
   val language_antiquotation: T
   val language_text: bool -> T
   val language_verbatim: bool -> T
   val language_latex: bool -> T
   val language_rail: T
   val language_path: T
   val language_mixfix: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val defN: string
   val refN: string
   val completionN: string val completion: T
   val no_completionN: string val no_completion: T
   val updateN: string val update: T
   val lineN: string
   val end_lineN: string
   val offsetN: string
   val end_offsetN: string
   val fileN: string
   val idN: string
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
   val block_properties: string list
   val indentN: string
   val widthN: string
   val blockN: string val block: bool -> int -> T
   val breakN: string val break: int -> int -> T
   val fbreakN: string val fbreak: T
   val itemN: string val item: T
   val wordsN: string val words: T
   val hiddenN: string val hidden: T
   val deleteN: string val delete: T
   val bash_functionN: string
   val scala_functionN: string
   val system_optionN: string
   val sessionN: string
   val theoryN: string
   val classN: string
   val type_nameN: string
   val constantN: string
   val fixedN: string val fixed: string -> T
   val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
   val literal_factN: string val literal_fact: string -> T
   val method_modifierN: string
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
   val skolemN: string val skolem: T
   val boundN: string val bound: T
   val varN: string val var: T
   val numeralN: string val numeral: T
   val literalN: string val literal: T
   val delimiterN: string val delimiter: T
   val inner_stringN: string val inner_string: T
   val inner_cartoucheN: string val inner_cartouche: T
   val token_rangeN: string val token_range: T
   val sortingN: string val sorting: T
   val typingN: string val typing: T
   val class_parameterN: string val class_parameter: T
   val ML_keyword1N: string val ML_keyword1: T
   val ML_keyword2N: string val ML_keyword2: T
   val ML_keyword3N: string val ML_keyword3: T
   val ML_delimiterN: string val ML_delimiter: T
   val ML_tvarN: string val ML_tvar: T
   val ML_numeralN: string val ML_numeral: T
   val ML_charN: string val ML_char: T
   val ML_stringN: string val ML_string: T
   val ML_commentN: string val ML_comment: T
   val ML_defN: string
   val ML_openN: string
   val ML_structureN: string
   val ML_typingN: string val ML_typing: T
   val ML_breakpointN: string val ML_breakpoint: int -> T
   val antiquotedN: string val antiquoted: T
   val antiquoteN: string val antiquote: T
   val file_typeN: string
   val antiquotationN: string
   val ML_antiquotationN: string
   val document_antiquotationN: string
   val document_antiquotation_optionN: string
   val raw_textN: string val raw_text: T
   val plain_textN: string val plain_text: T
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
   val document_markerN: string val document_marker: T
   val document_tagN: string val document_tag: string -> T
   val markdown_paragraphN: string val markdown_paragraph: T
   val markdown_itemN: string val markdown_item: T
   val markdown_bulletN: string val markdown_bullet: int -> T
   val markdown_listN: string val markdown_list: string -> T
   val itemizeN: string
   val enumerateN: string
   val descriptionN: string
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
   val commandN: string val command_properties: T -> T
   val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
   val verbatimN: string val verbatim: T
   val cartoucheN: string val cartouche: T
   val commentN: string val comment: T
   val keyword1N: string val keyword1: T
   val keyword2N: string val keyword2: T
   val keyword3N: string val keyword3: T
   val quasi_keywordN: string val quasi_keyword: T
   val improperN: string val improper: T
   val operatorN: string val operator: T
   val comment1N: string val comment1: T
   val comment2N: string val comment2: T
   val comment3N: string val comment3: T
   val elapsedN: string
   val cpuN: string
   val gcN: string
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
   val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time}
   val command_timingN: string
   val command_timing_properties:
     {file: string, offset: int, name: string} -> Time.time -> Properties.T
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
   val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
   val command_indentN: string val command_indent: int -> T
   val goalN: string val goal: T
   val subgoalN: string val subgoal: string -> T
   val taskN: string
   val forkedN: string val forked: T
   val joinedN: string val joined: T
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
   val canceledN: string val canceled: T
   val initializedN: string val initialized: T
   val finalizedN: string val finalized: T
   val consolidatingN: string val consolidating: T
   val consolidatedN: string val consolidated: T
   val exec_idN: string
   val initN: string
   val statusN: string val status: T
   val resultN: string val result: T
   val writelnN: string val writeln: T
   val stateN: string val state: T
   val informationN: string val information: T
   val tracingN: string val tracing: T
   val warningN: string val warning: T
   val legacyN: string val legacy: T
   val errorN: string val error: T
   val systemN: string val system: T
   val protocolN: string
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: unit -> T
   val intensifyN: string val intensify: T
   val browserN: string
   val graphviewN: string
   val theory_exportsN: string
   val sendbackN: string
   val paddingN: string
   val padding_line: Properties.entry
   val padding_command: Properties.entry
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val functionN: string
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
   val protocol_handler: string -> Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val ML_statistics: Properties.entry
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
+  val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val build_session_finished: Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
   val exportN: string
   type export_args =
    {id: string option,
     serial: serial,
     theory_name: string,
     name: string,
     executable: bool,
     compress: bool,
     strict: bool}
   val export: export_args -> Properties.T
   val debugger_state: string -> Properties.T
   val debugger_output: string -> Properties.T
   val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
   val simp_trace_hintN: string
   val simp_trace_ignoreN: string
   val simp_trace_cancel: serial -> Properties.T
   type output = Output.output * Output.output
   val no_output: output
   val add_mode: string -> (T -> output) -> unit
   val output: T -> output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markups: T list -> string -> string
   val markup_only: T -> string
   val markup_report: string -> string
 end;
 
 structure Markup: MARKUP =
 struct
 
 (** markup elements **)
 
 (* basic markup *)
 
 type T = string * Properties.T;
 
 val empty = ("", []);
 
 fun is_empty ("", _) = true
   | is_empty _ = false;
 
 
 fun properties more_props ((elem, props): T) =
   (elem, fold_rev Properties.put more_props props);
 
 fun markup_elem name = (name, (name, []): T);
 fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
 fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T);
 
 
 (* misc properties *)
 
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
 val xnameN = "xname";
 fun xname a = properties [(xnameN, a)];
 
 val kindN = "kind";
 
 val serialN = "serial";
 fun serial_properties i = [(serialN, Value.print_int i)];
 
 val instanceN = "instance";
 
 
 (* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *)
 
 val (meta_titleN, meta_title) = markup_elem "meta_title";
 val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
 val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
 val (meta_dateN, meta_date) = markup_elem "meta_date";
 val (meta_licenseN, meta_license) = markup_elem "meta_license";
 val (meta_descriptionN, meta_description) = markup_elem "meta_description";
 
 
 (* embedded languages *)
 
 val languageN = "language";
 val symbolsN = "symbols";
 val antiquotesN = "antiquotes";
 val delimitedN = "delimited"
 
 fun is_delimited props =
   Properties.get props delimitedN = SOME "true";
 
 fun language {name, symbols, antiquotes, delimited} =
   (languageN,
    [(nameN, name),
     (symbolsN, Value.print_bool symbols),
     (antiquotesN, Value.print_bool antiquotes),
     (delimitedN, Value.print_bool delimited)]);
 
 fun language' {name, symbols, antiquotes} delimited =
   language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
 
 val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false};
 val language_method =
   language {name = "method", symbols = true, antiquotes = false, delimited = false};
 val language_attribute =
   language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
 val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
 val language_type = language' {name = "type", symbols = true, antiquotes = false};
 val language_term = language' {name = "term", symbols = true, antiquotes = false};
 val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
 val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
 val language_document = language' {name = "document", symbols = false, antiquotes = true};
 val language_document_marker =
   language {name = "document_marker", symbols = true, antiquotes = true, delimited = true};
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
 val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
 val language_latex = language' {name = "latex", symbols = false, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
 val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
 val language_mixfix =
   language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
 
 
 (* formal entities *)
 
 val (bindingN, binding) = markup_elem "binding";
 
 val entityN = "entity";
 fun entity kind name =
   (entityN,
     (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
 
 val defN = "def";
 val refN = "ref";
 
 
 (* completion *)
 
 val (completionN, completion) = markup_elem "completion";
 val (no_completionN, no_completion) = markup_elem "no_completion";
 
 val (updateN, update) = markup_elem "update";
 
 
 (* position *)
 
 val lineN = "line";
 val end_lineN = "end_line";
 
 val offsetN = "offset";
 val end_offsetN = "end_offset";
 
 val fileN = "file";
 val idN = "id";
 
 val position_properties' = [fileN, idN];
 val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";
 
 
 (* expression *)
 
 val expressionN = "expression";
 fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]);
 
 
 (* citation *)
 
 val (citationN, citation) = markup_string "citation" nameN;
 
 
 (* external resources *)
 
 val (pathN, path) = markup_string "path" nameN;
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
 
 
 (* pretty printing *)
 
 val markupN = "markup";
 val consistentN = "consistent";
 val unbreakableN = "unbreakable";
 val indentN = "indent";
 
 val block_properties = [markupN, consistentN, unbreakableN, indentN];
 
 val widthN = "width";
 
 val blockN = "block";
 fun block c i =
   (blockN,
     (if c then [(consistentN, Value.print_bool c)] else []) @
     (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val breakN = "break";
 fun break w i =
   (breakN,
     (if w <> 0 then [(widthN, Value.print_int w)] else []) @
     (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val (fbreakN, fbreak) = markup_elem "fbreak";
 
 val (itemN, item) = markup_elem "item";
 
 
 (* text properties *)
 
 val (wordsN, words) = markup_elem "words";
 
 val (hiddenN, hidden) = markup_elem "hidden";
 
 val (deleteN, delete) = markup_elem "delete";
 
 
 (* misc entities *)
 
 val bash_functionN = "bash_function";
 val scala_functionN = "scala_function";
 val system_optionN = "system_option";
 
 val sessionN = "session";
 
 val theoryN = "theory";
 val classN = "class";
 val type_nameN = "type_name";
 val constantN = "constant";
 
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
 
 val method_modifierN = "method_modifier";
 
 
 (* inner syntax *)
 
 val (tfreeN, tfree) = markup_elem "tfree";
 val (tvarN, tvar) = markup_elem "tvar";
 val (freeN, free) = markup_elem "free";
 val (skolemN, skolem) = markup_elem "skolem";
 val (boundN, bound) = markup_elem "bound";
 val (varN, var) = markup_elem "var";
 val (numeralN, numeral) = markup_elem "numeral";
 val (literalN, literal) = markup_elem "literal";
 val (delimiterN, delimiter) = markup_elem "delimiter";
 val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche";
 
 val (token_rangeN, token_range) = markup_elem "token_range";
 
 val (sortingN, sorting) = markup_elem "sorting";
 val (typingN, typing) = markup_elem "typing";
 val (class_parameterN, class_parameter) = markup_elem "class_parameter";
 
 
 (* ML *)
 
 val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
 val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
 val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3";
 val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
 val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
 val (ML_charN, ML_char) = markup_elem "ML_char";
 val (ML_stringN, ML_string) = markup_elem "ML_string";
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
 
 val ML_defN = "ML_def";
 val ML_openN = "ML_open";
 val ML_structureN = "ML_structure";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
 val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN;
 
 
 (* antiquotations *)
 
 val (antiquotedN, antiquoted) = markup_elem "antiquoted";
 val (antiquoteN, antiquote) = markup_elem "antiquote";
 
 val file_typeN = "file_type";
 val antiquotationN = "antiquotation";
 val ML_antiquotationN = "ML_antiquotation";
 val document_antiquotationN = "document_antiquotation";
 val document_antiquotation_optionN = "document_antiquotation_option";
 
 
 (* document text *)
 
 val (raw_textN, raw_text) = markup_elem "raw_text";
 val (plain_textN, plain_text) = markup_elem "plain_text";
 
 val (paragraphN, paragraph) = markup_elem "paragraph";
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
 val (document_markerN, document_marker) = markup_elem "document_marker";
 val (document_tagN, document_tag) = markup_string "document_tag" nameN;
 
 
 (* Markdown document structure *)
 
 val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
 val (markdown_itemN, markdown_item) = markup_elem "markdown_item";
 val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
 val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
 
 val itemizeN = "itemize";
 val enumerateN = "enumerate";
 val descriptionN = "description";
 
 
 (* formal input *)
 
 val inputN = "input";
 fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props);
 
 
 (* outer syntax *)
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
 
 val commandN = "command"; val command_properties = properties [(kindN, commandN)];
 val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
 
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (keyword3N, keyword3) = markup_elem "keyword3";
 val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
 val (improperN, improper) = markup_elem "improper";
 val (operatorN, operator) = markup_elem "operator";
 val (stringN, string) = markup_elem "string";
 val (alt_stringN, alt_string) = markup_elem "alt_string";
 val (verbatimN, verbatim) = markup_elem "verbatim";
 val (cartoucheN, cartouche) = markup_elem "cartouche";
 val (commentN, comment) = markup_elem "comment";
 
 
 (* comments *)
 
 val (comment1N, comment1) = markup_elem "comment1";
 val (comment2N, comment2) = markup_elem "comment2";
 val (comment3N, comment3) = markup_elem "comment3";
 
 
 (* timing *)
 
 val elapsedN = "elapsed";
 val cpuN = "cpu";
 val gcN = "gc";
 
 fun timing_properties {elapsed, cpu, gc} =
  [(elapsedN, Value.print_time elapsed),
   (cpuN, Value.print_time cpu),
   (gcN, Value.print_time gc)];
 
 fun parse_timing_properties props =
  {elapsed = Properties.seconds props elapsedN,
   cpu = Properties.seconds props cpuN,
   gc = Properties.seconds props gcN};
 
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
 
 
 (* command timing *)
 
 val command_timingN = "command_timing";
 
 fun command_timing_properties {file, offset, name} elapsed =
  [(fileN, file), (offsetN, Value.print_int offset),
   (nameN, name), (elapsedN, Value.print_time elapsed)];
 
 fun parse_command_timing_properties props =
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>
       SOME ({file = file, offset = Value.parse_int offset, name = name},
         Properties.seconds props elapsedN)
   | _ => NONE);
 
 
 (* indentation *)
 
 val (command_indentN, command_indent) = markup_int "command_indent" indentN;
 
 
 (* goals *)
 
 val (goalN, goal) = markup_elem "goal";
 val (subgoalN, subgoal) = markup_string "subgoal" nameN;
 
 
 (* command status *)
 
 val taskN = "task";
 
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
 val (runningN, running) = markup_elem "running";
 val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
 val (canceledN, canceled) = markup_elem "canceled";
 val (initializedN, initialized) = markup_elem "initialized";
 val (finalizedN, finalized) = markup_elem "finalized";
 val (consolidatingN, consolidating) = markup_elem "consolidating";
 val (consolidatedN, consolidated) = markup_elem "consolidated";
 
 
 (* messages *)
 
 val exec_idN = "exec_id";
 
 val initN = "init";
 val (statusN, status) = markup_elem "status";
 val (resultN, result) = markup_elem "result";
 val (writelnN, writeln) = markup_elem "writeln";
 val (stateN, state) = markup_elem "state"
 val (informationN, information) = markup_elem "information";
 val (tracingN, tracing) = markup_elem "tracing";
 val (warningN, warning) = markup_elem "warning";
 val (legacyN, legacy) = markup_elem "legacy";
 val (errorN, error) = markup_elem "error";
 val (systemN, system) = markup_elem "system";
 val protocolN = "protocol";
 
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
 val badN = "bad";
 fun bad () = (badN, serial_properties (serial ()));
 
 val (intensifyN, intensify) = markup_elem "intensify";
 
 
 (* active areas *)
 
 val browserN = "browser"
 val graphviewN = "graphview";
 val theory_exportsN = "theory_exports";
 
 val sendbackN = "sendback";
 val paddingN = "padding";
 val padding_line = (paddingN, "line");
 val padding_command = (paddingN, "command");
 
 val dialogN = "dialog";
 fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]);
 
 val jedit_actionN = "jedit_action";
 
 
 (* protocol message functions *)
 
 val functionN = "function"
 
 val commands_accepted = [(functionN, "commands_accepted")];
 
 val assign_update = [(functionN, "assign_update")];
 val removed_versions = [(functionN, "removed_versions")];
 
 fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)];
 
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
 val ML_statistics = (functionN, "ML_statistics");
 
 val task_statistics = (functionN, "task_statistics");
 
 val command_timing = (functionN, "command_timing");
 
 val theory_timing = (functionN, "theory_timing");
 
+val session_timing = (functionN, "session_timing");
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   | dest_loading_theory _ = NONE;
 
 val build_session_finished = [("function", "build_session_finished")];
 
 val print_operationsN = "print_operations";
 val print_operations = [(functionN, print_operationsN)];
 
 
 (* export *)
 
 val exportN = "export";
 
 type export_args =
  {id: string option,
   serial: serial,
   theory_name: string,
   name: string,
   executable: bool,
   compress: bool,
   strict: bool};
 
 fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) =
  [(functionN, exportN),
   (idN, the_default "" id),
   (serialN, Value.print_int serial),
   ("theory_name", theory_name),
   (nameN, name),
   ("executable", Value.print_bool executable),
   ("compress", Value.print_bool compress),
   ("strict", Value.print_bool strict)];
 
 
 (* debugger *)
 
 fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)];
 fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
 
 
 (* simplifier trace *)
 
 val simp_trace_panelN = "simp_trace_panel";
 
 val simp_trace_logN = "simp_trace_log";
 val simp_trace_stepN = "simp_trace_step";
 val simp_trace_recurseN = "simp_trace_recurse";
 val simp_trace_hintN = "simp_trace_hint";
 val simp_trace_ignoreN = "simp_trace_ignore";
 
 fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)];
 
 
 
 (** print mode operations **)
 
 type output = Output.output * Output.output;
 
 val no_output = ("", "");
 
 local
   val default = {output = Output_Primitives.markup_fn};
   val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
 in
   fun add_mode name output =
     Synchronized.change modes (fn tab =>
       (if not (Symtab.defined tab name) then ()
        else Output.warning ("Redefining markup mode " ^ quote name);
        Symtab.update (name, {output = output}) tab));
   fun get_mode () =
     the_default default
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;
 
 fun markup m =
   let val (bg, en) = output m
   in Library.enclose (Output.escape bg) (Output.escape en) end;
 
 val markups = fold_rev markup;
 
 fun markup_only m = markup m "";
 
 fun markup_report "" = ""
   | markup_report txt = markup report txt;
 
 end;
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,692 +1,693 @@
 /*  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"
 
   class Function(val name: String)
   {
     val PROPERTY: Properties.Entry = (FUNCTION, name)
   }
 
   class Properties_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
         case PROPERTY :: args => Some(args)
         case _ => None
       }
   }
 
   class Name_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[(String)] =
       props match {
         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
+  object Session_Timing extends Properties_Function("session_timing")
   object ML_Statistics extends Properties_Function("ML_statistics")
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Name_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
   object Protocol_Handler extends Name_Function("protocol_handler")
 
   object Commands_Accepted extends Function("commands_accepted")
   object Assign_Update extends Function("assign_update")
   object Removed_Versions extends Function("removed_versions")
 
   object Invoke_Scala extends Function("invoke_scala")
   {
     def unapply(props: Properties.T): Option[(String, String)] =
       props match {
         case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
 
   object Cancel_Scala extends Function("cancel_scala")
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (ID, id)) => Some(id)
         case _ => None
       }
   }
 
   val PRINT_OPERATIONS = "print_operations"
 
 
   /* export */
 
   val EXPORT = "export"
   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/System/process_result.scala b/src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala
+++ b/src/Pure/System/process_result.scala
@@ -1,80 +1,81 @@
 /*  Title:      Pure/System/process_result.scala
     Author:     Makarius
 
 Result of system process.
 */
 
 package isabelle
 
 object Process_Result
 {
   def print_return_code(rc: Int): String = "Return code: " + rc + rc_text(rc)
   def print_rc(rc: Int): String = "return code " + rc + rc_text(rc)
 
   def rc_text(rc: Int): String =
     return_code_text.get(rc) match {
       case None => ""
       case Some(text) => " (" + text + ")"
     }
   private val return_code_text =
     Map(0 -> "OK",
       1 -> "ERROR",
       2 -> "FAILURE",
       130 -> "INTERRUPT",
       131 -> "QUIT SIGNAL",
       137 -> "KILL SIGNAL",
       138 -> "BUS ERROR",
       139 -> "SEGMENTATION VIOLATION",
       143 -> "TERMINATION SIGNAL")
 }
 
 final case class Process_Result(
   rc: Int,
   out_lines: List[String] = Nil,
   err_lines: List[String] = Nil,
   timeout: Boolean = false,
   timing: Timing = Timing.zero)
 {
   def out: String = cat_lines(out_lines)
   def err: String = cat_lines(err_lines)
 
   def output(outs: List[String]): Process_Result =
     copy(out_lines = out_lines ::: outs.flatMap(split_lines))
   def errors(errs: List[String]): Process_Result =
     copy(err_lines = err_lines ::: errs.flatMap(split_lines))
-  def error(err: String): Process_Result = errors(List(err))
+  def error(err: String): Process_Result =
+    if (err.isEmpty) this else errors(List(err))
 
   def was_timeout: Process_Result = copy(rc = 1, timeout = true)
 
   def ok: Boolean = rc == 0
   def interrupted: Boolean = rc == Exn.Interrupt.return_code
 
   def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1)
 
   def check_rc(pred: Int => Boolean): Process_Result =
     if (pred(rc)) this
     else if (interrupted) throw Exn.Interrupt()
     else Exn.error(err)
 
   def check: Process_Result = check_rc(_ == 0)
 
   def print_return_code: String = Process_Result.print_return_code(rc)
   def print_rc: String = Process_Result.print_rc(rc)
 
   def print: Process_Result =
   {
     Output.warning(err)
     Output.writeln(out)
     copy(out_lines = Nil, err_lines = Nil)
   }
 
   def print_stdout: Process_Result =
   {
     Output.warning(err, stdout = true)
     Output.writeln(out, stdout = true)
     copy(out_lines = Nil, err_lines = Nil)
   }
 
   def print_if(b: Boolean): Process_Result = if (b) print else this
   def print_stdout_if(b: Boolean): Process_Result = if (b) print_stdout else this
 }
diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML
+++ b/src/Pure/Tools/build.ML
@@ -1,271 +1,273 @@
 (*  Title:      Pure/Tools/build.ML
     Author:     Makarius
 
 Build Isabelle sessions.
 *)
 
 signature BUILD =
 sig
   val build: string -> unit
 end;
 
 structure Build: BUILD =
 struct
 
 (* command timings *)
 
 type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name, time*)
 
 val empty_timings: timings = Symtab.empty;
 
 fun update_timings props =
   (case Markup.parse_command_timing_properties props of
     SOME ({file, offset, name}, time) =>
       Symtab.map_default (file, Inttab.empty)
         (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
   | NONE => I);
 
 fun approximative_id name pos =
   (case (Position.file_of pos, Position.offset_of pos) of
     (SOME file, SOME offset) =>
       if name = "" then NONE else SOME {file = file, offset = offset, name = name}
   | _ => NONE);
 
 fun get_timings timings tr =
   (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
     SOME {file, offset, name} =>
       (case Symtab.lookup timings file of
         SOME offsets =>
           (case Inttab.lookup offsets offset of
             SOME (name', time) => if name = name' then SOME time else NONE
           | NONE => NONE)
       | NONE => NONE)
   | NONE => NONE)
   |> the_default Time.zeroTime;
 
 
 (* session timing *)
 
 fun session_timing session_name verbose f x =
   let
     val start = Timing.start ();
     val y = f x;
     val timing = Timing.result start;
 
     val threads = string_of_int (Multithreading.max_threads ());
     val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
       |> Real.fmt (StringCvt.FIX (SOME 2));
 
     val timing_props =
       [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
-    val _ = Protocol_Message.marker "Timing" timing_props;
+    val _ = Output.protocol_message (Markup.session_timing :: timing_props) [];
     val _ =
       if verbose then
         Output.physical_stderr ("Timing " ^ session_name ^ " (" ^
           threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
       else ();
   in y end;
 
 
 (* protocol messages *)
 
 fun protocol_message props output =
   (case props of
     function :: args =>
       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
         Protocol_Message.marker (#2 function) args
       else if function = Markup.command_timing then
         let
           val name = the_default "" (Properties.get args Markup.nameN);
           val pos = Position.of_properties args;
           val {elapsed, ...} = Markup.parse_timing_properties args;
           val is_significant =
             Timing.is_relevant_time elapsed andalso
             elapsed >= Options.default_seconds "command_timing_threshold";
         in
           if is_significant then
             (case approximative_id name pos of
               SOME id =>
                 Protocol_Message.marker (#2 function)
                   (Markup.command_timing_properties id elapsed)
             | NONE => ())
           else ()
         end
       else if function = Markup.theory_timing then
         Protocol_Message.marker (#2 function) args
+      else if function = Markup.session_timing then
+        Protocol_Message.marker "Timing" args
       else
         (case Markup.dest_loading_theory props of
           SOME name => Protocol_Message.marker_text "loading_theory" name
         | NONE => Export.protocol_message props output)
   | [] => raise Output.Protocol_Message props);
 
 
 (* build theories *)
 
 fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
   let
     val context =
       {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
         last_timing = last_timing};
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
   in
     if null conds then
       (Options.set_default options;
         Isabelle_Process.init_options ();
         Future.fork I;
         (Thy_Info.use_theories context qualifier master_dir
         |>
           (case Options.string options "profiling" of
             "" => I
           | "time" => profile_time
           | "allocations" => profile_allocations
           | bad => error ("Bad profiling option: " ^ quote bad))
         |> Unsynchronized.setmp print_mode
             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
     else
       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
         " (undefined " ^ commas conds ^ ")\n")
   end;
 
 
 (* build session *)
 
 datatype args = Args of
  {pide: bool,
   symbol_codes: (string * int) list,
   command_timings: Properties.T list,
   verbose: bool,
   browser_info: Path.T,
   document_files: (Path.T * Path.T) list,
   graph_file: Path.T,
   parent_name: string,
   chapter: string,
   session_name: string,
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
   session_positions: (string * Properties.T) list,
   session_directories: (string * string) list,
   doc_names: string list,
   global_theories: (string * string) list,
   loaded_theories: string list,
   bibtex_entries: string list};
 
 fun decode_args pide yxml =
   let
     open XML.Decode;
     val position = Position.of_properties o properties;
     val (symbol_codes, (command_timings, (verbose, (browser_info,
       (document_files, (graph_file, (parent_name, (chapter, (session_name, (master_dir,
       (theories, (session_positions, (session_directories, (doc_names, (global_theories,
       (loaded_theories, bibtex_entries)))))))))))))))) =
       pair (list (pair string int)) (pair (list properties) (pair bool (pair string
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
           (pair string
             (pair (((list (pair Options.decode (list (pair string position))))))
               (pair (list (pair string properties))
                 (pair (list (pair string string)) (pair (list string)
                   (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {pide = pide, symbol_codes = symbol_codes, command_timings = command_timings,
       verbose = verbose, browser_info = Path.explode browser_info,
       document_files = map (apply2 Path.explode) document_files,
       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
       session_name = session_name, master_dir = Path.explode master_dir, theories = theories,
       session_positions = session_positions, session_directories = session_directories,
       doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
       bibtex_entries = bibtex_entries}
   end;
 
 fun build_session (Args {pide, symbol_codes, command_timings, verbose, browser_info, document_files,
     graph_file, parent_name, chapter, session_name, master_dir, theories, session_positions,
     session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
     val _ =
       Resources.init_session
         {pide = pide,
          session_positions = session_positions,
          session_directories = session_directories,
          docs = doc_names,
          global_theories = global_theories,
          loaded_theories = loaded_theories};
 
     val _ =
       Session.init
         symbols
         (Options.default_bool "browser_info")
         browser_info
         (Options.default_string "document")
         (Options.default_string "document_output")
         (Present.document_variants (Options.default ()))
         document_files
         graph_file
         parent_name
         (chapter, session_name)
         verbose;
 
     val last_timing = get_timings (fold update_timings command_timings empty_timings);
 
     val res1 =
       theories |>
         (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir)
           |> session_timing session_name verbose
           |> Exn.capture);
     val res2 = Exn.capture Session.finish ();
 
     val _ = Resources.finish_session_base ();
     val _ = Par_Exn.release_all [res1, res2];
     val _ =
       if session_name = Context.PureN
       then Theory.install_pure (Thy_Info.get_theory Context.PureN) else ();
   in () end;
 
 
 (* command-line tool *)
 
 fun inline_errors exn =
   Runtime.exn_message_list exn
   |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg));
 
 fun build args_file =
   let
     val _ = SHA1.test_samples ();
     val _ = Options.load_default ();
     val _ = Isabelle_Process.init_options ();
     val args = decode_args false (File.read (Path.explode args_file));
     val _ =
       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
         build_session args
       handle exn => (inline_errors exn; Exn.reraise exn);
     val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined;
     val _ = Options.reset_default ();
   in () end;
 
 
 (* PIDE version *)
 
 val _ =
   Isabelle_Process.protocol_command "build_session"
     (fn [args_yxml] =>
         let
           val args = decode_args true args_yxml;
           fun exec e =
             if can Theory.get_pure () then
               Isabelle_Thread.fork
                 {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (),
                   interrupts = false} e
               |> ignore
             else e ();
         in
           exec (fn () =>
             (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
               ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
           |> let open XML.Encode in pair int (list string) end
           |> Output.protocol_message Markup.build_session_finished)
         end
       | _ => raise Match);
 
 end;
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,948 +1,956 @@
 /*  Title:      Pure/Tools/build.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Build and manage Isabelle sessions.
 */
 
 package isabelle
 
 
 import scala.collection.{SortedSet, mutable}
 import scala.annotation.tailrec
 
 
 object Build
 {
   /** auxiliary **/
 
   /* persistent build info */
 
   sealed case class Session_Info(
     sources: String,
     input_heaps: List[String],
     output_heap: Option[String],
     return_code: Int)
   {
     def ok: Boolean = return_code == 0
   }
 
 
   /* queue with scheduling information */
 
   private object Queue
   {
     type Timings = (List[Properties.T], Double)
 
     def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
     {
       val no_timings: Timings = (Nil, 0.0)
 
       store.access_database(session_name) match {
         case None => no_timings
         case Some(db) =>
           def ignore_error(msg: String) =
           {
             progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
             no_timings
           }
           try {
             val command_timings = store.read_command_timings(db, session_name)
             val session_timing =
               store.read_session_timing(db, session_name) match {
                 case Markup.Elapsed(t) => t
                 case _ => 0.0
               }
             (command_timings, session_timing)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
             case _: XML.Error => ignore_error("")
           }
           finally { db.close }
       }
     }
 
     def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
       : Map[String, Double] =
     {
       val maximals = sessions_structure.build_graph.maximals.toSet
       def desc_timing(session_name: String): Double =
       {
         if (maximals.contains(session_name)) timing(session_name)
         else {
           val descendants = sessions_structure.build_descendants(List(session_name)).toSet
           val g = sessions_structure.build_graph.restrict(descendants)
           (0.0 :: g.maximals.flatMap(desc => {
             val ps = g.all_preds(List(desc))
             if (ps.exists(p => !timing.isDefinedAt(p))) None
             else Some(ps.map(timing(_)).sum)
           })).max
         }
       }
       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
     }
 
     def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
       : Queue =
     {
       val graph = sessions_structure.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
         make_session_timing(sessions_structure,
           timings.map({ case (name, (_, t)) => (name, t) }).toMap)
 
       object Ordering extends scala.math.Ordering[String]
       {
         def compare_timing(name1: String, name2: String): Int =
         {
           val t1 = session_timing(name1)
           val t2 = session_timing(name2)
           if (t1 == 0.0 || t2 == 0.0) 0
           else t1 compare t2
         }
 
         def compare(name1: String, name2: String): Int =
           compare_timing(name2, name1) match {
             case 0 =>
               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
                 case ord => ord
               }
             case ord => ord
           }
       }
 
       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
     }
   }
 
   private class Queue(
     graph: Graph[String, Sessions.Info],
     order: SortedSet[String],
     val command_timings: String => List[Properties.T])
   {
     def is_inner(name: String): Boolean = !graph.is_maximal(name)
 
     def is_empty: Boolean = graph.is_empty
 
     def - (name: String): Queue =
       new Queue(graph.del_node(name),
         order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
         command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
     {
       val it = order.iterator.dropWhile(name =>
         skip(name)
           || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
           || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
       else None
     }
   }
 
 
   /* PIDE protocol handler */
 
   /* job: running prover process */
 
   private class Job(progress: Progress,
     session_name: String,
     val info: Sessions.Info,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_store: Boolean,
     verbose: Boolean,
     val numa_node: Option[Int],
     command_timings: List[Properties.T])
   {
     val options: Options = NUMA.policy_options(info.options, numa_node)
 
     private val sessions_structure = deps.sessions_structure
 
     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display)
 
     private val export_tmp_dir = Isabelle_System.tmp_dir("export")
     private val export_consumer =
       Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
 
     private val future_result: Future[Process_Result] =
       Future.thread("build", uninterruptible = true) {
         val parent = info.parent.getOrElse("")
         val base = deps(parent)
         val args_yxml =
           YXML.string_of_body(
             {
               import XML.Encode._
               pair(list(pair(string, int)), pair(list(properties), pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(pair(string, properties)))),
                 pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
                 pair(list(string), pair(list(pair(string, string)),
                 pair(list(string), list(string)))))))))))))))))(
               (Symbol.codes, (command_timings, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (session_name, (Path.current,
                 (info.theories,
                 (sessions_structure.session_positions,
                 (sessions_structure.dest_session_directories,
                 (base.doc_names, (base.global_theories.toList,
                 (base.loaded_theories.keys, info.bibtex_entries.map(_.info))))))))))))))))))
             })
 
         val env =
           Isabelle_System.settings() +
             ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
 
         val is_pure = Sessions.is_pure(session_name)
 
         val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
 
         val eval_store =
           if (do_store) {
             (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
             List("ML_Heap.save_child " +
               ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
           }
           else Nil
 
         if (options.bool("pide_session")) {
           val resources = new Resources(sessions_structure, deps(parent))
           val session =
             new Session(options, resources) {
               override val xml_cache: XML.Cache = store.xml_cache
               override val xz_cache: XZ.Cache = store.xz_cache
             }
 
           val build_session_errors: Promise[List[String]] = Future.promise
           val stdout = new StringBuilder(1000)
+          val stderr = new StringBuilder(1000)
           val messages = new mutable.ListBuffer[XML.Elem]
           val command_timings = new mutable.ListBuffer[Properties.T]
           val theory_timings = new mutable.ListBuffer[Properties.T]
+          val session_timings = new mutable.ListBuffer[Properties.T]
           val runtime_statistics = new mutable.ListBuffer[Properties.T]
           val task_statistics = new mutable.ListBuffer[Properties.T]
 
           def fun(
             name: String,
             acc: mutable.ListBuffer[Properties.T],
             unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
           {
             name -> ((msg: Prover.Protocol_Output) =>
               unapply(msg.properties) match {
                 case Some(props) => acc += props; true
                 case _ => false
               })
           }
 
           session.init_protocol_handler(new Session.Protocol_Handler
             {
               override def exit() { build_session_errors.cancel }
 
               private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
               {
                 val (rc, errors) =
                   try {
                     val (rc, errs) =
                     {
                       import XML.Decode._
                       pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
                     }
                     val errors =
                       for (err <- errs) yield {
                         val prt = Protocol_Message.expose_no_reports(err)
                         Pretty.string_of(prt, metric = Symbol.Metric)
                       }
                     (rc, errors)
                   }
                   catch { case ERROR(err) => (2, List(err)) }
 
                 session.protocol_command("Prover.stop", rc.toString)
                 build_session_errors.fulfill(errors)
                 true
               }
 
               private def loading_theory(msg: Prover.Protocol_Output): Boolean =
                 msg.properties match {
                   case Markup.Loading_Theory(name) =>
                     progress.theory(Progress.Theory(name, session = session_name))
                     true
                   case _ => false
                 }
 
               private def export(msg: Prover.Protocol_Output): Boolean =
                 msg.properties match {
                   case Protocol.Export(args) =>
                     export_consumer(session_name, args, msg.bytes)
                     true
                   case _ => false
                 }
 
               val functions =
                 List(
                   Markup.Build_Session_Finished.name -> build_session_finished,
                   Markup.Loading_Theory.name -> loading_theory,
                   Markup.EXPORT -> export,
                   fun(Markup.Command_Timing.name, command_timings, Markup.Command_Timing.unapply),
                   fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
+                  fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
                   fun(Markup.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply),
                   fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
             })
 
           session.all_messages += Session.Consumer[Any]("build_session_output")
             {
               case msg: Prover.Output =>
                 val message = msg.message
                 if (msg.is_stdout) {
                   stdout ++= Symbol.encode(XML.content(message))
                 }
+                else if (msg.is_stderr) {
+                  stderr ++= Symbol.encode(XML.content(message))
+                }
                 else if (Protocol.is_exported(message)) {
                   messages += message
                 }
               case _ =>
             }
 
           val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
           val process =
             Isabelle_Process(session, options, sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env)
 
           val errors =
             Isabelle_Thread.interrupt_handler(_ => process.terminate) {
               Exn.capture { process.await_startup } match {
                 case Exn.Res(_) =>
                   session.protocol_command("build_session", args_yxml)
                   build_session_errors.join_result
                 case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
               }
             }
 
           val process_result =
             Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
           val process_output =
             stdout.toString ::
             messages.toList.map(message =>
               Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
+            session_timings.toList.map(Protocol.Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
 
-          val result = process_result.output(process_output)
+          val result =
+            process_result.output(process_output).error(Library.trim_line(stderr.toString))
 
           errors match {
             case Exn.Res(Nil) => result
             case Exn.Res(errs) =>
               result.error_rc.output(
                 errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
                   errs.map(Protocol.Error_Message_Marker.apply))
             case Exn.Exn(Exn.Interrupt()) =>
               if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
             case Exn.Exn(exn) => throw exn
           }
         }
         else {
           val args_file = Isabelle_System.tmp_file("build")
           File.write(args_file, args_yxml)
 
           val eval_build =
             "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file))
           val eval_main = Command_Line.ML_tool(eval_build :: eval_store)
 
           val process =
             ML_Process(options, deps.sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
 
           Isabelle_Thread.interrupt_handler(_ => process.terminate) {
             process.result(
               progress_stdout =
                 {
                   case Protocol.Loading_Theory_Marker(theory) =>
                     progress.theory(Progress.Theory(theory, session = session_name))
                   case Protocol.Export.Marker((args, path)) =>
                     val body =
                       try { Bytes.read(path) }
                       catch {
                         case ERROR(msg) =>
                           error("Failed to read export " + quote(args.compound_name) + "\n" + msg)
                       }
                     path.file.delete
                     export_consumer(session_name, args, body)
                   case _ =>
                 },
               progress_limit =
                 options.int("process_output_limit") match {
                   case 0 => None
                   case m => Some(m * 1000000L)
                 },
               strict = false)
           }
         }
       }
 
     def terminate: Unit = future_result.cancel
     def is_finished: Boolean = future_result.is_finished
 
     private val timeout_request: Option[Event_Timer.Request] =
     {
       if (info.timeout > Time.zero)
         Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
       else None
     }
 
     def join: (Process_Result, Option[String]) =
     {
       val result0 = future_result.join
       val result1 =
         export_consumer.shutdown(close = true).map(Output.error_message_text) match {
           case Nil => result0
           case errs => result0.errors(errs).error_rc
         }
 
       Isabelle_System.rm_tree(export_tmp_dir)
 
       if (result1.ok)
         Present.finish(progress, store.browser_info, graph_file, info, session_name)
 
       graph_file.delete
 
       val was_timeout =
         timeout_request match {
           case None => false
           case Some(request) => !request.cancel
         }
 
       val result2 =
         if (result1.interrupted) {
           if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
           else result1.error(Output.error_message_text("Interrupt"))
         }
         else result1
 
       val heap_digest =
         if (result2.ok && do_store && store.output_heap(session_name).is_file)
           Some(Sessions.write_heap_digest(store.output_heap(session_name)))
         else None
 
       (result2, heap_digest)
     }
   }
 
 
 
   /** build with results **/
 
   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   {
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def info(name: String): Sessions.Info = results(name)._2
     val rc: Int =
       (0 /: results.iterator.map(
         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
     def ok: Boolean = rc == 0
 
     override def toString: String = rc.toString
   }
 
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
     progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Sessions.Info] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     soft_build: Boolean = false,
     verbose: Boolean = false,
     export_files: Boolean = false): Results =
   {
     val build_options =
       options +
         "ML_statistics" +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
         "pide_reports=false"
 
     val store = Sessions.store(build_options)
 
     Isabelle_Fonts.init()
 
 
     /* session selection and dependencies */
 
     val full_sessions =
       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
 
     def sources_stamp(deps: Sessions.Deps, session_name: String): String =
     {
       val digests =
         full_sessions(session_name).meta_digest ::
         deps.sources(session_name) :::
         deps.imported_sources(session_name)
       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
     }
 
     val deps =
     {
       val deps0 =
         Sessions.deps(full_sessions.selection(selection),
           progress = progress, inlined_files = true, verbose = verbose,
           list_files = list_files, check_keywords = check_keywords).check_errors
 
       if (soft_build && !fresh_build) {
         val outdated =
           deps0.sessions_structure.build_topological_order.flatMap(name =>
             store.access_database(name) match {
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
                   if build.ok && build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
                 }
               case None => Some(name)
             })
 
         Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
           progress = progress, inlined_files = true).check_errors
       }
       else deps0
     }
 
 
     /* check unknown files */
 
     if (check_unknown_files) {
       val source_files =
         (for {
           (_, base) <- deps.session_bases.iterator
           (path, _) <- base.sources.iterator
         } yield path).toList
       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
       val unknown_files =
         Mercurial.check_files(source_files)._2.
           filterNot(path => exclude_files.contains(path.canonical_file))
       if (unknown_files.nonEmpty) {
         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
       }
     }
 
 
     /* main build process */
 
     val queue = Queue(progress, deps.sessions_structure, store)
 
     store.prepare_output_dir()
 
     if (clean_build) {
       for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)
           else progress.echo(name + " FAILED to clean")
         }
       }
     }
 
     // scheduler loop
     case class Result(
       current: Boolean,
       heap_digest: Option[String],
       process: Option[Process_Result],
       info: Sessions.Info)
     {
       def ok: Boolean =
         process match {
           case None => false
           case Some(res) => res.rc == 0
         }
     }
 
     def sleep()
     {
       Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
     }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
     @tailrec def loop(
       pending: Queue,
       running: Map[String, (List[String], Job)],
       results: Map[String, Result]): Map[String, Result] =
     {
       def used_node(i: Int): Boolean =
         running.iterator.exists(
           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
 
       if (pending.is_empty) results
       else {
         if (progress.stopped) {
           for ((_, (_, job)) <- running) job.terminate
         }
 
         running.find({ case (_, (_, job)) => job.is_finished }) match {
           case Some((session_name, (input_heaps, job))) =>
             //{{{ finish job
 
             val (process_result, heap_digest) = job.join
 
             val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail =
             {
               val tail = job.info.options.int("process_output_tail")
               process_result.copy(
                 out_lines =
                   "(see also " + store.output_log(session_name).file.toString + ")" ::
                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
             }
 
 
             // write log file
             if (process_result.ok) {
               File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
             }
             else File.write(store.output_log(session_name), terminate_lines(log_lines))
 
             // write database
             {
               val build_log =
                 Build_Log.Log_File(session_name, process_result.out_lines).
                   parse_session_info(
                     command_timings = true,
                     theory_timings = true,
                     ml_statistics = true,
                     task_statistics = true)
 
               using(store.open_database(session_name, output = true))(db =>
                 store.write_session_info(db, session_name,
                   build_log =
                     if (process_result.timeout) build_log.error("Timeout") else build_log,
                   build =
                     Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
                       process_result.rc)))
             }
 
             // messages
             process_result.err_lines.foreach(progress.echo)
 
             if (process_result.ok)
               progress.echo(
                 "Finished " + session_name + " (" + process_result.timing.message_resources + ")")
             else {
               progress.echo(session_name + " FAILED")
               if (!process_result.interrupted) progress.echo(process_result_tail.out)
             }
 
             loop(pending - session_name, running - session_name,
               results +
                 (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt) match {
               case Some((session_name, info)) =>
                 val ancestor_results =
                   deps.sessions_structure.build_requirements(List(session_name)).
                     filterNot(_ == session_name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
 
                 val (current, heap_digest) =
                 {
                   store.access_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>
                           val heap_digest = store.find_heap_digest(session_name)
                           val current =
                             !fresh_build &&
                             build.ok &&
                             build.sources == sources_stamp(deps, session_name) &&
                             build.input_heaps == ancestor_heaps &&
                             build.output_heap == heap_digest &&
                             !(do_store && heap_digest.isEmpty)
                           (current, heap_digest)
                         case None => (false, None)
                       }
                     case None => (false, None)
                   }
                 }
                 val all_current = current && ancestor_results.forall(_.current)
 
                 if (all_current)
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
 
                   store.clean_output(session_name)
                   using(store.open_database(session_name, output = true))(
                     store.init_session_info(_, session_name))
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Job(progress, session_name, info, deps, store, do_store, verbose,
                       numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
                 else {
                   progress.echo(session_name + " CANCELLED")
                   loop(pending - session_name, running,
                     results + (session_name -> Result(false, heap_digest, None, info)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
             ///}}}
           case None => sleep(); loop(pending, running, results)
         }
       }
     }
 
 
     /* build results */
 
     val results0 =
       if (deps.is_empty) {
         progress.echo_warning("Nothing to build")
         Map.empty[String, Result]
       }
       else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
 
     val results =
       new Results(
         (for ((name, result) <- results0.iterator)
           yield (name, (result.process, result.info))).toMap)
 
     if (export_files) {
       for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
         val info = results.info(name)
         if (info.export_files.nonEmpty) {
           progress.echo("Exporting " + info.name + " ...")
           for ((dir, prune, pats) <- info.export_files) {
             Export.export_files(store, name, info.dir + dir,
               progress = if (verbose) progress else new Progress,
               export_prune = prune,
               export_patterns = pats)
           }
         }
       }
     }
 
     if (results.rc != 0 && (verbose || !no_build)) {
       val unfinished =
         (for {
           name <- results.sessions.iterator
           if !results(name).ok
          } yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
 
 
     /* global browser info */
 
     if (!no_build) {
       val browser_chapters =
         (for {
           (name, result) <- results0.iterator
           if result.ok
           info = full_sessions(name)
           if info.options.bool("browser_info")
         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
 
       for ((chapter, entries) <- browser_chapters)
         Present.update_chapter_index(store.browser_info, chapter, entries)
 
       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
     }
 
     results
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   {
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var numa_shuffling = false
     var requirements = false
     var soft_build = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
     var build_heap = false
     var clean_build = false
     var dirs: List[Path] = Nil
     var export_files = false
     var fresh_build = false
     var session_groups: List[String] = Nil
     var max_jobs = 1
     var check_keywords: Set[String] = Set.empty
     var list_files = false
     var no_build = false
     var options = Options.init(opts = build_options)
     var verbose = false
     var exclude_sessions: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -R           refer to requirements of selected sessions
     -S           soft build: only observe changes of sources, not heap images
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           build heap images
     -c           clean build
     -d DIR       include session directory
     -e           export files from session specification into file-system
     -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- test dependencies only
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
   Build and manage Isabelle sessions, depending on implicit settings:
 
 """ + Library.prefix_lines("  ",  Build_Log.Settings.show()) + "\n",
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
       "R" -> (_ => requirements = true),
       "S" -> (_ => soft_build = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "b" -> (_ => build_heap = true),
       "c" -> (_ => clean_build = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "e" -> (_ => export_files = true),
       "f" -> (_ => fresh_build = true),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "k:" -> (arg => check_keywords = check_keywords + arg),
       "l" -> (_ => list_files = true),
       "n" -> (_ => no_build = true),
       "o:" -> (arg => options = options + arg),
       "v" -> (_ => verbose = true),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
     val sessions = getopts(args)
 
     val progress = new Console_Progress(verbose = verbose)
 
     val start_date = Date.now()
 
     if (verbose) {
       progress.echo(
         "Started at " + Build_Log.print_date(start_date) +
           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
       progress.echo(Build_Log.Settings.show() + "\n")
     }
 
     val results =
       progress.interrupt_handler {
         build(options,
           selection = Sessions.Selection(
             requirements = requirements,
             all_sessions = all_sessions,
             base_sessions = base_sessions,
             exclude_session_groups = exclude_session_groups,
             exclude_sessions = exclude_sessions,
             session_groups = session_groups,
             sessions = sessions),
           progress = progress,
           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
           build_heap = build_heap,
           clean_build = clean_build,
           dirs = dirs,
           select_dirs = select_dirs,
           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
           max_jobs = max_jobs,
           list_files = list_files,
           check_keywords = check_keywords,
           fresh_build = fresh_build,
           no_build = no_build,
           soft_build = soft_build,
           verbose = verbose,
           export_files = export_files)
       }
     val end_date = Date.now()
     val elapsed_time = end_date.time - start_date.time
 
     if (verbose) {
       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
     }
 
     val total_timing =
       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
         copy(elapsed = elapsed_time)
     progress.echo(total_timing.message_resources)
 
     sys.exit(results.rc)
   })
 
 
   /* build logic image */
 
   def build_logic(options: Options, logic: String,
     progress: Progress = new Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
     fresh: Boolean = false,
     strict: Boolean = false): Int =
   {
     val selection = Sessions.Selection.session(logic)
     val rc =
       if (!fresh && build(options, selection = selection,
             build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
         Build.build(options, selection = selection, progress = progress,
           build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
       }
     if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
   }
 }