diff --git a/src/Pure/ML/ml_statistics.scala b/src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala
+++ b/src/Pure/ML/ml_statistics.scala
@@ -1,284 +1,284 @@
 /*  Title:      Pure/ML/ml_statistics.scala
     Author:     Makarius
 
 ML runtime statistics.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.swing.{Frame, Component}
 
 import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
 import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
 import org.jfree.chart.plot.PlotOrientation
 
 
 object ML_Statistics
 {
   /* properties */
 
   val Now = new Properties.Double("now")
   def now(props: Properties.T): Double = Now.unapply(props).get
 
 
   /* monitor process */
 
   def monitor(pid: Long,
     delay: Time = Time.seconds(0.5),
     consume: Properties.T => Unit = Console.println)
   {
     def progress_stdout(line: String)
     {
       val props =
         Library.space_explode(',', line).flatMap((entry: String) =>
           Library.space_explode('=', entry) match {
             case List(a, b) => Some((a, b))
             case _ => None
           })
       if (props.nonEmpty) consume(props)
     }
 
     Bash.process("exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
         Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
           ML_Syntax.print_double(delay.seconds)),
         cwd = Path.explode("~~").file)
       .result(progress_stdout = progress_stdout, strict = false).check
   }
 
 
   /* protocol handler */
 
   class Protocol_Handler extends Session.Protocol_Handler
   {
     private var session: Session = null
     private var monitoring: Future[Unit] = Future.value(())
 
     override def init(init_session: Session): Unit = synchronized
     {
       session = init_session
     }
 
     override def exit(): Unit = synchronized
     {
       session = null
       monitoring.cancel
     }
 
     private def consume(props: Properties.T): Unit = synchronized
     {
       if (session != null && session.session_options.bool("ML_statistics")) {
         session.runtime_statistics.post(Session.Runtime_Statistics(props))
       }
     }
 
-    private def ml_pid(msg: Prover.Protocol_Output): Boolean = synchronized
+    private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized
     {
       msg.properties match {
-        case Markup.ML_Pid(pid) =>
+        case Markup.ML_Statistics(pid) =>
           monitoring = Future.thread("ML_statistics") { monitor(pid, consume = consume) }
           true
         case _ => false
       }
     }
 
-    val functions = List(Markup.ML_Pid.name -> ml_pid)
+    val functions = List(Markup.ML_Statistics.name -> ml_statistics)
   }
 
 
   /* memory fields (mega bytes) */
 
   def mem_print(x: Long): Option[String] =
     if (x == 0L) None else Some(x.toString + " M")
 
   def mem_scale(x: Long): Long = x / 1024 / 1024
 
   def mem_field_scale(name: String, x: Double): Double =
     if (heap_fields._2.contains(name) || program_fields._2.contains(name))
       mem_scale(x.toLong).toDouble
     else x
 
   val CODE_SIZE = "size_code"
   val STACK_SIZE = "size_stacks"
   val HEAP_SIZE = "size_heap"
 
 
   /* standard fields */
 
   type Fields = (String, List[String])
 
   val tasks_fields: Fields =
     ("Future tasks",
       List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive",
         "tasks_urgent", "tasks_total"))
 
   val workers_fields: Fields =
     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
 
   val GC_fields: Fields =
     ("GCs", List("partial_GCs", "full_GCs", "share_passes"))
 
   val heap_fields: Fields =
     ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
       "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
 
   val program_fields: Fields =
     ("Program", List("size_code", "size_stacks"))
 
   val threads_fields: Fields =
     ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
       "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
 
   val time_fields: Fields =
     ("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC"))
 
   val speed_fields: Fields =
     ("Speed", List("speed_CPU", "speed_GC"))
 
   private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC")
 
 
   val all_fields: List[Fields] =
     List(tasks_fields, workers_fields, GC_fields, heap_fields, program_fields, threads_fields,
       time_fields, speed_fields)
 
   val main_fields: List[Fields] =
     List(tasks_fields, workers_fields, heap_fields)
 
 
   /* content interpretation */
 
   final case class Entry(time: Double, data: Map[String, Double])
   {
     def get(field: String): Double = data.getOrElse(field, 0.0)
   }
 
   val empty: ML_Statistics = apply(Nil)
 
   def apply(ml_statistics: List[Properties.T], heading: String = "",
     domain: String => Boolean = (key: String) => true): ML_Statistics =
   {
     require(ml_statistics.forall(props => Now.unapply(props).isDefined))
 
     val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
     val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
 
     val fields =
       SortedSet.empty[String] ++
         (for {
           props <- ml_statistics.iterator
           (x, _) <- props.iterator
           if x != Now.name && domain(x) } yield x)
 
     val content =
     {
       var last_edge = Map.empty[String, (Double, Double, Double)]
       val result = new mutable.ListBuffer[ML_Statistics.Entry]
       for (props <- ml_statistics) {
         val time = now(props) - time_start
         require(time >= 0.0)
 
         // rising edges -- relative speed
         val speeds =
           (for {
             (key, value) <- props.iterator
             key1 <- time_speed.get(key)
             if domain(key1)
           } yield {
             val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0))
 
             val x1 = time
             val y1 = java.lang.Double.parseDouble(value)
             val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
 
             if (y1 > y0) {
               last_edge += (key -> (x1, y1, s1))
               (key1, s1.toString)
             }
             else (key1, s0.toString)
           }).toList
 
         val data =
           SortedMap.empty[String, Double] ++
             (for {
               (x, y) <- props.iterator ++ speeds.iterator
               if x != Now.name && domain(x)
               z = java.lang.Double.parseDouble(y) if z != 0.0
             } yield { (x.intern, mem_field_scale(x, z)) })
 
         result += ML_Statistics.Entry(time, data)
       }
       result.toList
     }
 
     new ML_Statistics(heading, fields, content, time_start, duration)
   }
 }
 
 final class ML_Statistics private(
   val heading: String,
   val fields: Set[String],
   val content: List[ML_Statistics.Entry],
   val time_start: Double,
   val duration: Double)
 {
   /* content */
 
   def maximum(field: String): Double =
     (0.0 /: content)({ case (m, e) => m max e.get(field) })
 
   def average(field: String): Double =
   {
     @tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double =
       list match {
         case Nil => acc
         case e :: es =>
           val t = e.time
           sum(t, es, (t - t0) * e.get(field) + acc)
       }
     content match {
       case Nil => 0.0
       case List(e) => e.get(field)
       case e :: es => sum(e.time, es, 0.0) / duration
     }
   }
 
 
   /* charts */
 
   def update_data(data: XYSeriesCollection, selected_fields: List[String])
   {
     data.removeAllSeries
     for (field <- selected_fields) {
       val series = new XYSeries(field)
       content.foreach(entry => series.add(entry.time, entry.get(field)))
       data.addSeries(series)
     }
   }
 
   def chart(title: String, selected_fields: List[String]): JFreeChart =
   {
     val data = new XYSeriesCollection
     update_data(data, selected_fields)
 
     ChartFactory.createXYLineChart(title, "time", "value", data,
       PlotOrientation.VERTICAL, true, true, true)
   }
 
   def chart(fields: ML_Statistics.Fields): JFreeChart =
     chart(fields._1, fields._2)
 
   def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
     fields.map(chart).foreach(c =>
       GUI_Thread.later {
         new Frame {
           iconImage = GUI.isabelle_image()
           title = heading
           contents = Component.wrap(new ChartPanel(c))
           visible = true
         }
       })
 }
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,785 +1,782 @@
 (*  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_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 ml_pid: int -> Properties.T
+  val ML_statistics: {pid: int} -> Properties.T
   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 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)];
 
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
 
 
 (* command timing *)
 
 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"
 
-fun ml_pid pid = [(functionN, "ML_pid"), (idN, Value.print_int pid)];
+fun ML_statistics {pid} = [(functionN, "ML_statistics"), ("pid", Value.print_int pid)];
 
 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)];
 
 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,710 +1,709 @@
 /*  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
       }
 
     def parse(props: Properties.T): isabelle.Timing =
       unapply(props) getOrElse isabelle.Timing.zero
   }
 
   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 ML_Pid extends Function("ML_pid")
+  object ML_Statistics extends Function("ML_statistics")
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
-        case List(PROPERTY, (ID, Value.Long(pid))) => Some(pid)
+        case List(PROPERTY, ("pid", Value.Long(pid))) => Some(pid)
         case _ => None
       }
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
   {
     val Threads = new Properties.Int("threads")
   }
-  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/PIDE/session.scala b/src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala
+++ b/src/Pure/PIDE/session.scala
@@ -1,750 +1,747 @@
 /*  Title:      Pure/PIDE/session.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 PIDE editor session, potentially with running prover process.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.Queue
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 
 object Session
 {
   /* outlets */
 
   object Consumer
   {
     def apply[A](name: String)(consume: A => Unit): Consumer[A] =
       new Consumer[A](name, consume)
   }
   final class Consumer[-A] private(val name: String, val consume: A => Unit)
 
   class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
   {
     private val consumers = Synchronized[List[Consumer[A]]](Nil)
 
     def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
     def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
 
     def post(a: A)
     {
       for (c <- consumers.value.iterator) {
         dispatcher.send(() =>
           try { c.consume(a) }
           catch {
             case exn: Throwable =>
               Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
           })
       }
     }
   }
 
 
   /* change */
 
   sealed case class Change(
     previous: Document.Version,
     syntax_changed: List[Document.Node.Name],
     deps_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
     consolidate: List[Document.Node.Name],
     version: Document.Version)
 
   case object Change_Flush
 
 
   /* events */
 
   //{{{
   case class Command_Timing(props: Properties.T)
   case class Theory_Timing(props: Properties.T)
   case class Runtime_Statistics(props: Properties.T)
   case class Task_Statistics(props: Properties.T)
   case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
   case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
   sealed abstract class Phase
   {
     def print: String =
       this match {
         case Terminated(result) => if (result.ok) "finished" else "failed"
         case _ => Word.lowercase(this.toString)
       }
   }
   case object Inactive extends Phase  // stable
   case object Startup extends Phase  // transient
   case object Ready extends Phase  // metastable
   case object Shutdown extends Phase  // transient
   case class Terminated(result: Process_Result) extends Phase  // stable
   //}}}
 
 
   /* syslog */
 
   private[Session] class Syslog(limit: Int)
   {
     private var queue = Queue.empty[XML.Elem]
     private var length = 0
 
     def += (msg: XML.Elem): Unit = synchronized {
       queue = queue.enqueue(msg)
       length += 1
       if (length > limit) queue = queue.dequeue._2
     }
 
     def content: String = synchronized {
       cat_lines(queue.iterator.map(XML.content)) +
       (if (length > limit) "\n(A total of " + length + " messages...)" else "")
     }
   }
 
 
   /* protocol handlers */
 
   type Protocol_Function = Prover.Protocol_Output => Boolean
 
   abstract class Protocol_Handler
   {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
     val functions: List[(String, Protocol_Function)]
   }
 }
 
 
 class Session(_session_options: => Options, val resources: Resources) extends Document.Session
 {
   session =>
 
   val xml_cache: XML.Cache = XML.make_cache()
   val xz_cache: XZ.Cache = XZ.make_cache()
 
 
   /* global flags */
 
   @volatile var timing: Boolean = false
   @volatile var verbose: Boolean = false
 
 
   /* dynamic session options */
 
   def session_options: Options = _session_options
 
   def output_delay: Time = session_options.seconds("editor_output_delay")
   def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay")
   def prune_delay: Time = session_options.seconds("editor_prune_delay")
   def prune_size: Int = session_options.int("editor_prune_size")
   def syslog_limit: Int = session_options.int("editor_syslog_limit")
   def reparse_limit: Int = session_options.int("editor_reparse_limit")
 
 
   /* dispatcher */
 
   private val dispatcher =
     Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
 
   def assert_dispatcher[A](body: => A): A =
   {
     assert(dispatcher.check_thread)
     body
   }
 
   def require_dispatcher[A](body: => A): A =
   {
     require(dispatcher.check_thread)
     body
   }
 
   def send_dispatcher(body: => Unit): Unit =
   {
     if (dispatcher.check_thread) body
     else dispatcher.send(() => body)
   }
 
   def send_wait_dispatcher(body: => Unit): Unit =
   {
     if (dispatcher.check_thread) body
     else dispatcher.send_wait(() => body)
   }
 
 
   /* outlets */
 
   val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher)
   val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher)
   val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher)
   val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher)
   val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
   val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
   val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher)
   val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher)
   val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
   val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
   val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
   val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
   val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher)
 
   val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck!
 
 
   /** main protocol manager **/
 
   /* internal messages */
 
   private case class Start(start_prover: Prover.Receiver => Prover)
   private case object Stop
   private case class Get_State(promise: Promise[Document.State])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Update_Options(options: Options)
   private case object Consolidate_Execution
   private case object Prune_History
 
 
   /* phase */
 
   private def post_phase(new_phase: Session.Phase): Session.Phase =
   {
     phase_changed.post(new_phase)
     new_phase
   }
   private val _phase = Synchronized[Session.Phase](Session.Inactive)
   private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase))
 
   def phase: Session.Phase = _phase.value
   def is_ready: Boolean = phase == Session.Ready
 
 
   /* syslog */
 
   private val syslog = new Session.Syslog(syslog_limit)
   def syslog_content(): String = syslog.content
 
 
   /* pipelined change parsing */
 
   private case class Text_Edits(
     previous: Future[Document.Version],
     doc_blobs: Document.Blobs,
     text_edits: List[Document.Edit_Text],
     consolidate: List[Document.Node.Name],
     version_result: Promise[Document.Version])
 
   private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
   {
     case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
       val prev = previous.get_finished
       val change =
         Timing.timeit("parse_change", timing) {
           resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
         }
       version_result.fulfill(change.version)
       manager.send(change)
       true
   }
 
 
   /* buffered changes */
 
   private object change_buffer
   {
     private var assignment: Boolean = false
     private var nodes: Set[Document.Node.Name] = Set.empty
     private var commands: Set[Command] = Set.empty
 
     def flush(): Unit = synchronized {
       if (assignment || nodes.nonEmpty || commands.nonEmpty)
         commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
       if (nodes.nonEmpty) consolidation.update(nodes)
       assignment = false
       nodes = Set.empty
       commands = Set.empty
     }
     private val delay_flush = Delay.first(output_delay) { flush() }
 
     def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
       synchronized {
         assignment |= assign
         for (node <- edited_nodes) {
           nodes += node
         }
         for (command <- cmds) {
           nodes += command.node_name
           command.blobs_names.foreach(nodes += _)
           commands += command
         }
         delay_flush.invoke()
       }
 
     def shutdown()
     {
       delay_flush.revoke()
       flush()
     }
   }
 
 
   /* postponed changes */
 
   private object postponed_changes
   {
     private var postponed: List[Session.Change] = Nil
 
     def store(change: Session.Change): Unit = synchronized { postponed ::= change }
 
     def flush(state: Document.State): List[Session.Change] = synchronized {
       val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
       postponed = unassigned
       assigned.reverse
     }
   }
 
 
   /* node consolidation */
 
   private object consolidation
   {
     private val delay =
       Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) }
 
     private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
     private val state = Synchronized(init_state)
 
     def exit()
     {
       delay.revoke()
       state.change(_ => None)
     }
 
     def update(new_nodes: Set[Document.Node.Name] = Set.empty)
     {
       val active =
         state.change_result(st =>
           (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)))
       if (active) delay.invoke()
     }
 
     def flush(): Set[Document.Node.Name] =
       state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None))
   }
 
 
   /* prover process */
 
   private object prover
   {
     private val variable = Synchronized[Option[Prover]](None)
 
     def defined: Boolean = variable.value.isDefined
     def get: Prover = variable.value.get
     def set(p: Prover) { variable.change(_ => Some(p)) }
     def reset { variable.change(_ => None) }
     def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) }
   }
 
 
   /* file formats */
 
   lazy val file_formats: File_Format.Session =
     File_Format.registry.start_session(session)
 
 
   /* protocol handlers */
 
   private val protocol_handlers = Protocol_Handlers.init(session)
 
   def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
     protocol_handlers.get(name)
 
   def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
     protocol_handlers.init(handler)
 
   def init_protocol_handler(name: String): Unit =
     protocol_handlers.init(name)
 
 
   /* debugger */
 
   private val debugger_handler = new Debugger.Handler(this)
   init_protocol_handler(debugger_handler)
 
   def debugger: Debugger = debugger_handler.debugger
 
 
   /* manager thread */
 
   private val delay_prune =
     Delay.first(prune_delay) { manager.send(Prune_History) }
 
   private val manager: Consumer_Thread[Any] =
   {
     /* global state */
     val global_state = Synchronized(Document.State.init)
 
 
     /* raw edits */
 
     def handle_raw_edits(
       doc_blobs: Document.Blobs = Document.Blobs.empty,
       edits: List[Document.Edit_Text] = Nil,
       consolidate: List[Document.Node.Name] = Nil)
     //{{{
     {
       require(prover.defined)
 
       if (edits.nonEmpty) prover.get.discontinue_execution()
 
       val previous = global_state.value.history.tip.version
       val version = Future.promise[Document.Version]
       global_state.change(_.continue_history(previous, edits, version))
 
       raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
       change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version))
     }
     //}}}
 
 
     /* resulting changes */
 
     def handle_change(change: Session.Change)
     //{{{
     {
       require(prover.defined)
 
       // define commands
       {
         val id_commands = new mutable.ListBuffer[Command]
         def id_command(command: Command)
         {
           for {
             (name, digest) <- command.blobs_defined
             if !global_state.value.defined_blob(digest)
           } {
             change.version.nodes(name).get_blob match {
               case Some(blob) =>
                 global_state.change(_.define_blob(digest))
                 prover.get.define_blob(digest, blob.bytes)
               case None =>
                 Output.error_message("Missing blob " + quote(name.toString))
             }
           }
 
           if (!global_state.value.defined_command(command.id)) {
             global_state.change(_.define_command(command))
             id_commands += command
           }
         }
         for { (_, edit) <- change.doc_edits } {
           edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) })
         }
         if (id_commands.nonEmpty) prover.get.define_commands_bulk(id_commands.toList)
       }
 
       val assignment = global_state.value.the_assignment(change.previous).check_finished
       global_state.change(_.define_version(change.version, assignment))
 
       prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
       resources.commit(change)
     }
     //}}}
 
 
     /* prover output */
 
     def handle_output(output: Prover.Output)
     //{{{
     {
       def bad_output()
       {
         if (verbose)
           Output.warning("Ignoring bad prover output: " + output.message.toString)
       }
 
       def change_command(f: Document.State => (Command.State, Document.State))
       {
         try {
           val st = global_state.change_result(f)
           change_buffer.invoke(false, Nil, List(st.command))
         }
         catch { case _: Document.State.Fail => bad_output() }
       }
 
       output match {
         case msg: Prover.Protocol_Output =>
           val handled = protocol_handlers.invoke(msg)
           if (!handled) {
             msg.properties match {
               case Markup.Protocol_Handler(name) if prover.defined =>
                 init_protocol_handler(name)
 
               case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
                 command_timings.post(Session.Command_Timing(props))
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
                 change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))
 
-              case Markup.ML_Statistics(props) =>
-                runtime_statistics.post(Session.Runtime_Statistics(props))
-
               case Markup.Task_Statistics(props) =>
                 task_statistics.post(Session.Task_Statistics(props))
 
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 val id = Value.Long.unapply(args.id.get).get
                 val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
                 change_command(_.add_export(id, (args.serial, export)))
 
               case List(Markup.Commands_Accepted.PROPERTY) =>
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
                     ids.foreach(id =>
                       change_command(_.accumulate(id, Protocol.Commands_Accepted.message, xml_cache)))
                   case _ => bad_output()
                 }
 
               case List(Markup.Assign_Update.PROPERTY) =>
                 msg.text match {
                   case Protocol.Assign_Update(id, edited, update) =>
                     try {
                       val (edited_nodes, cmds) =
                         global_state.change_result(_.assign(id, edited, update))
                       change_buffer.invoke(true, edited_nodes, cmds)
                       manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
                   case _ => bad_output()
                 }
                 delay_prune.invoke()
 
               case List(Markup.Removed_Versions.PROPERTY) =>
                 msg.text match {
                   case Protocol.Removed(removed) =>
                     try {
                       global_state.change(_.removed_versions(removed))
                       manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
                   case _ => bad_output()
                 }
 
               case _ => bad_output()
             }
           }
         case _ =>
           output.properties match {
             case Position.Id(state_id) =>
               change_command(_.accumulate(state_id, output.message, xml_cache))
 
             case _ if output.is_init =>
               prover.get.options(file_formats.prover_options(session_options))
               prover.get.init_session(resources)
               phase = Session.Ready
               debugger.ready()
 
             case Markup.Process_Result(result) if output.is_exit =>
               if (prover.defined) protocol_handlers.exit()
               file_formats.stop_session
               phase = Session.Terminated(result)
               prover.reset
 
             case _ =>
               raw_output_messages.post(output)
           }
         }
     }
     //}}}
 
 
     /* main thread */
 
     Consumer_Thread.fork[Any]("Session.manager", daemon = true)
     {
       case arg: Any =>
         //{{{
         arg match {
           case output: Prover.Output =>
             if (output.is_syslog) {
               syslog += output.message
               syslog_messages.post(output)
             }
 
             if (output.is_stdout || output.is_stderr)
               raw_output_messages.post(output)
             else handle_output(output)
 
             all_messages.post(output)
 
           case input: Prover.Input =>
             all_messages.post(input)
 
           case Start(start_prover) if !prover.defined =>
             prover.set(start_prover(manager.send(_)))
 
           case Stop =>
             consolidation.exit()
             delay_prune.revoke()
             if (prover.defined) {
               global_state.change(_ => Document.State.init)
               prover.get.terminate
             }
 
           case Get_State(promise) =>
             promise.fulfill(global_state.value)
 
           case Consolidate_Execution =>
             if (prover.defined) {
               val state = global_state.value
               state.stable_tip_version match {
                 case None => consolidation.update()
                 case Some(version) =>
                   val consolidate =
                     consolidation.flush().iterator.filter(name =>
                       !resources.session_base.loaded_theory(name) &&
                       !state.node_consolidated(version, name) &&
                       state.node_maybe_consolidated(version, name)).toList
                   if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate)
               }
             }
 
           case Prune_History =>
             if (prover.defined) {
               val old_versions = global_state.change_result(_.remove_versions(prune_size))
               if (old_versions.nonEmpty) prover.get.remove_versions(old_versions)
             }
 
           case Update_Options(options) =>
             if (prover.defined && is_ready) {
               prover.get.options(file_formats.prover_options(options))
               handle_raw_edits()
             }
             global_options.post(Session.Global_Options(options))
 
           case Cancel_Exec(exec_id) if prover.defined =>
             prover.get.cancel_exec(exec_id)
 
           case Session.Raw_Edits(doc_blobs, edits) if prover.defined =>
             handle_raw_edits(doc_blobs = doc_blobs, edits = edits)
 
           case Session.Dialog_Result(id, serial, result) if prover.defined =>
             prover.get.dialog_result(serial, result)
             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
 
           case Protocol_Command(name, args) if prover.defined =>
             prover.get.protocol_command_args(name, args)
 
           case change: Session.Change if prover.defined =>
             val state = global_state.value
             if (!state.removing_versions && state.is_assigned(change.previous))
               handle_change(change)
             else postponed_changes.store(change)
 
           case Session.Change_Flush if prover.defined =>
             val state = global_state.value
             if (!state.removing_versions)
               postponed_changes.flush(state).foreach(handle_change)
 
           case bad =>
             if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
         }
         true
         //}}}
     }
   }
 
 
   /* main operations */
 
   def get_state(): Document.State =
   {
     if (manager.is_active) {
       val promise = Future.promise[Document.State]
       manager.send_wait(Get_State(promise))
       promise.join
     }
     else Document.State.init
   }
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
     get_state().snapshot(name, pending_edits)
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
     resources.session_base.overall_syntax
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot =
   {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
       output_delay.sleep
       await_stable_snapshot()
     }
     else snapshot
   }
 
   def start(start_prover: Prover.Receiver => Prover)
   {
     file_formats
     _phase.change(
       {
         case Session.Inactive =>
           manager.send(Start(start_prover))
           post_phase(Session.Startup)
         case phase => error("Cannot start prover in phase " + quote(phase.print))
       })
   }
 
   def stop(): Process_Result =
   {
     val was_ready =
       _phase.guarded_access(
         {
           case Session.Startup | Session.Shutdown => None
           case Session.Terminated(_) => Some((false, phase))
           case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
           case Session.Ready => Some((true, post_phase(Session.Shutdown)))
         })
     if (was_ready) manager.send(Stop)
     prover.await_reset()
 
     change_parser.shutdown()
     change_buffer.shutdown()
     manager.shutdown()
     dispatcher.shutdown()
 
     phase match {
       case Session.Terminated(result) => result
       case phase => error("Bad session phase after shutdown: " + quote(phase.print))
     }
   }
 
   def protocol_command(name: String, args: String*)
   { manager.send(Protocol_Command(name, args.toList)) }
 
   def cancel_exec(exec_id: Document_ID.Exec)
   { manager.send(Cancel_Exec(exec_id)) }
 
   def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   {
     if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits))
   }
 
   def update_options(options: Options)
   { manager.send_wait(Update_Options(options)) }
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   { manager.send(Session.Dialog_Result(id, serial, result)) }
 }
diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML
+++ b/src/Pure/System/isabelle_process.ML
@@ -1,262 +1,262 @@
 (*  Title:      Pure/System/isabelle_process.ML
     Author:     Makarius
 
 Isabelle process wrapper.
 *)
 
 signature ISABELLE_PROCESS =
 sig
   val is_active: unit -> bool
   exception STOP of int
   val protocol_command: string -> (string list -> unit) -> unit
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
   val init_options: unit -> unit
   val init_options_interactive: unit -> unit
   val init: unit -> unit
   val init_build: unit -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
 struct
 
 (* print mode *)
 
 val isabelle_processN = "isabelle_process";
 
 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
 
 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
 
 val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
 
 
 (* protocol commands *)
 
 exception STOP of int;
 
 val is_protocol_exn = fn STOP _ => true | _ => false;
 
 local
 
 val commands =
   Synchronized.var "Isabelle_Process.commands"
     (Symtab.empty: (string list -> unit) Symtab.table);
 
 in
 
 fun protocol_command name cmd =
   Synchronized.change commands (fn cmds =>
    (if not (Symtab.defined cmds name) then ()
     else warning ("Redefining Isabelle protocol command " ^ quote name);
     Symtab.update (name, cmd) cmds));
 
 fun run_command name args =
   (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
       (Runtime.exn_trace_system (fn () => cmd args)
         handle exn =>
           if is_protocol_exn exn then Exn.reraise exn
           else error ("Isabelle protocol command failure: " ^ quote name)));
 
 end;
 
 
 (* restricted tracing messages *)
 
 val tracing_messages =
   Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
 
 fun reset_tracing exec_id =
   Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
 
 fun update_tracing () =
   (case Position.parse_id (Position.thread_data ()) of
     NONE => ()
   | SOME exec_id =>
       let
         val ok =
           Synchronized.change_result tracing_messages (fn tab =>
             let
               val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
               val limit = Options.default_int "editor_tracing_messages";
               val ok = limit <= 0 orelse n <= limit;
             in (ok, Inttab.update (exec_id, n) tab) end);
       in
         if ok then ()
         else
           let
             val (text, promise) = Active.dialog_text ();
             val _ =
               writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
                 text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
             val m = Value.parse_int (Future.join promise)
               handle Fail _ => error "Stopped";
           in
             Synchronized.change tracing_messages
               (Inttab.map_default (exec_id, 0) (fn k => k - m))
           end
       end);
 
 
 (* init protocol -- uninterruptible *)
 
 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
 
 local
 
 fun recover crash =
   (Synchronized.change crashes (cons crash);
     Output.physical_stderr
       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
 
 val _ = Session.protocol_handler "isabelle.ML_Statistics$Protocol_Handler";
 
 in
 
 fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
   let
     val _ = SHA1.test_samples ()
       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
 
     val _ = Output.physical_stderr Symbol.STX;
 
 
     (* streams *)
 
     val (in_stream, out_stream) = Socket_IO.open_streams address;
     val _ = Byte_Message.write_line out_stream password;
 
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
     val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
 
 
     (* messages *)
 
     val msg_channel = Message_Channel.make out_stream;
 
     fun message name props body =
       Message_Channel.send msg_channel (Message_Channel.message name props body);
 
     fun standard_message props name ss =
       if forall (fn s => s = "") ss then ()
       else
         let
           val props' =
             (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
               (false, SOME id') => props @ [(Markup.idN, id')]
             | _ => props);
         in message name props' (XML.blob ss) end;
 
     fun report_message ss =
       if Context_Position.pide_reports ()
       then standard_message [] Markup.reportN ss else ();
 
     val serial_props = Markup.serial_properties o serial;
 
     val message_context =
       Unsynchronized.setmp Private_Output.status_fn (standard_message [] Markup.statusN) #>
       Unsynchronized.setmp Private_Output.report_fn report_message #>
       Unsynchronized.setmp Private_Output.result_fn
         (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #>
       Unsynchronized.setmp Private_Output.writeln_fn
         (fn s => standard_message (serial_props ()) Markup.writelnN s) #>
       Unsynchronized.setmp Private_Output.state_fn
         (fn s => standard_message (serial_props ()) Markup.stateN s) #>
       Unsynchronized.setmp Private_Output.information_fn
         (fn s => standard_message (serial_props ()) Markup.informationN s) #>
       Unsynchronized.setmp Private_Output.tracing_fn
         (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #>
       Unsynchronized.setmp Private_Output.warning_fn
         (fn s => standard_message (serial_props ()) Markup.warningN s) #>
       Unsynchronized.setmp Private_Output.legacy_fn
         (fn s => standard_message (serial_props ()) Markup.legacyN s) #>
       Unsynchronized.setmp Private_Output.error_message_fn
         (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #>
       Unsynchronized.setmp Private_Output.system_message_fn
         (fn ss => message Markup.systemN [] (XML.blob ss)) #>
       Unsynchronized.setmp Private_Output.protocol_message_fn
         (fn props => fn body => message Markup.protocolN props body) #>
       Unsynchronized.setmp print_mode
         ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes));
 
 
     (* protocol *)
 
     fun protocol_loop () =
       let
         val _ =
           (case Byte_Message.read_message in_stream of
             NONE => raise STOP 0
           | SOME [] => Output.system_message "Isabelle process: no input"
           | SOME (name :: args) => run_command name args)
           handle exn =>
             if is_protocol_exn exn then Exn.reraise exn
             else (Runtime.exn_system_message exn handle crash => recover crash);
       in protocol_loop () end;
 
     fun protocol () =
      (Session.init_protocol_handlers ();
-      Output.protocol_message (Markup.ml_pid (ML_Pid.get ())) [];
+      Output.protocol_message (Markup.ML_statistics {pid = ML_Pid.get ()}) [];
       message Markup.initN [] [XML.Text (Session.welcome ())];
       protocol_loop ());
 
     val result = Exn.capture (message_context protocol) ();
 
 
     (* shutdown *)
 
     val _ = Future.shutdown ();
     val _ = Execution.reset ();
     val _ = Message_Channel.shutdown msg_channel;
     val _ = BinIO.closeIn in_stream;
     val _ = BinIO.closeOut out_stream;
 
     val _ = Options.reset_default ();
   in
     (case result of
       Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
     | _ => Exn.release result)
   end);
 
 end;
 
 
 (* init options *)
 
 fun init_options () =
  (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   let val proofs = Options.default_int "record_proofs"
   in if proofs < 0 then () else Proofterm.proofs := proofs end;
   Printer.show_markup_default := false);
 
 fun init_options_interactive () =
  (init_options ();
   Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
   Printer.show_markup_default := true);
 
 
 (* generic init *)
 
 fun init_modes modes =
   let
     val address = Options.default_string \<^system_option>\<open>system_channel_address\<close>;
     val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>;
   in
     if address <> "" andalso password <> ""
     then init_protocol modes (address, password)
     else init_options ()
   end;
 
 fun init () = init_modes (protocol_modes1, protocol_modes2);
 fun init_build () = init_modes ([], protocol_modes2);
 
 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,953 +1,957 @@
 /*  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_timings0: 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_timings0, (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
 
         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
           }
 
         object Build_Session_Errors
         {
           private val promise: Promise[List[String]] = Future.promise
 
           def result: Exn.Result[List[String]] = promise.join_result
           def cancel: Unit = promise.cancel
           def apply(errs: List[String])
           {
             try { promise.fulfill(errs) }
             catch { case _: IllegalStateException => }
           }
         }
 
         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(errors)
               true
             }
 
             private def loading_theory(msg: Prover.Protocol_Output): Boolean =
               msg.properties match {
                 case Markup.Loading_Theory(name) =>
                   progress.theory(Progress.Theory(name, session = session_name))
                   true
                 case _ => false
               }
 
             private def export(msg: Prover.Protocol_Output): Boolean =
               msg.properties match {
                 case Protocol.Export(args) =>
                   export_consumer(session_name, args, msg.bytes)
                   true
                 case _ => false
               }
 
             private def command_timing(props: Properties.T): Option[Properties.T] =
               for {
                 props1 <- Markup.Command_Timing.unapply(props)
                 elapsed <- Markup.Elapsed.unapply(props1)
                 elapsed_time = Time.seconds(elapsed)
                 if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
               } yield props1.filter(p => Markup.command_timing_properties(p._1))
 
             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, command_timing),
                 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.runtime_statistics += Session.Consumer("ML_statistics")
+          {
+            case Session.Runtime_Statistics(props) => runtime_statistics += props
+          }
+
         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
               }
               else if (msg.is_exit) {
                 val err =
                   "Prover terminated" +
                     (msg.properties match {
                       case Markup.Process_Result(result) => ": " + result.print_rc
                       case _ => ""
                     })
                 Build_Session_Errors(List(err))
               }
             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.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.Session_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).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
         }
       }
 
     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 session_finished(session_name: String, process_result: Process_Result): String =
     "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
 
   def session_timing(session_name: String, build_log: Build_Log.Session_Info): String =
   {
     val props = build_log.session_timing
     val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
     val timing = Markup.Timing_Properties.parse(props)
     "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
   }
 
   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)))
             }
 
             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)
 
             // 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
             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) {
               if (verbose) progress.echo(session_timing(session_name, build_log))
               progress.echo(session_finished(session_name, process_result))
             }
             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
   }
 }