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,861 +1,861 @@
 (*  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: bool -> T
   val language_url: bool -> 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 positionN: string val position: T
   val position_properties: string list
   val position_property: Properties.entry -> bool
   val def_name: string -> string
   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 toolN: string val tool: 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 load_commandN: string
   val bash_functionN: string
   val scala_functionN: string
   val system_optionN: string
   val sessionN: string
   val theoryN: string
   val classN: string
   val localeN: string
   val bundleN: string
   val type_nameN: string
   val constantN: string
   val axiomN: string
   val factN: string
   val oracleN: 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 attributeN: string
   val methodN: string
   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 document_latexN: string val document_latex: T
   val latex_outputN: string val latex_output: T
   val latex_macro0N: string val latex_macro0: string -> T
   val latex_macroN: string val latex_macro: string -> T
   val latex_environmentN: string val latex_environment: string -> T
   val latex_headingN: string val latex_heading: string -> T
   val latex_bodyN: string val latex_body: string -> T
   val latex_index_itemN: string val latex_index_item: T
   val latex_index_entryN: string val latex_index_entry: string -> T
   val latex_delimN: string val latex_delim: string -> T
   val latex_tagN: string val latex_tag: string -> T
   val optional_argumentN: string val optional_argument: string -> T -> 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 command_spanN: string val command_span: string -> 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 countN: string
   val ML_profiling_entryN: string
   val ML_profiling_entry: {name: string, count: int} -> T
   val ML_profilingN: string
   val ML_profiling: string -> 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 function: string -> Properties.entry
   val ML_statistics: {pid: int, stats_dir: string} -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   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_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};
 val language_url = language' {name = "url", symbols = false, antiquotes = false};
 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 (positionN, position) = markup_elem "position";
 
 val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
 fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
 
 (* position "def" names *)
 
 fun make_def a = "def_" ^ a;
 
 val def_names = Symtab.make (map (fn a => (a, make_def a)) position_properties);
 
 fun def_name a =
   (case Symtab.lookup def_names a of
     SOME b => b
   | NONE => make_def a);
 
 
 (* 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;
 val (toolN, tool) = markup_string "tool" 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 load_commandN = "load_command";
 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 localeN = "locale";
 val bundleN = "bundle";
 val type_nameN = "type_name";
 val constantN = "constant";
 val axiomN = "axiom";
 val factN = "fact";
 val oracleN = "oracle";
 
 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 attributeN = "attribute";
 val methodN = "method";
 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;
 
 
 (* LaTeX *)
 
 val (document_latexN, document_latex) = markup_elem "document_latex";
 
 val (latex_outputN, latex_output) = markup_elem "latex_output";
 val (latex_macro0N, latex_macro0) = markup_string "latex_macro0" nameN;
 val (latex_macroN, latex_macro) = markup_string "latex_macro" nameN;
 val (latex_environmentN, latex_environment) = markup_string "latex_environment" nameN;
 val (latex_headingN, latex_heading) = markup_string "latex_heading" kindN;
 val (latex_bodyN, latex_body) = markup_string "latex_body" kindN;
 val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item";
 val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN;
 val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN;
 val (latex_tagN, latex_tag) = markup_string "latex_tag" nameN;
 
 val optional_argumentN = "optional_argument";
 fun optional_argument arg = properties [(optional_argumentN, arg)];
 
 
 (* 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 (command_spanN, command_span) = markup_string "command_span" nameN;
 
 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";
 
 
 (* ML profiling *)
 
 val countN = "count";
 
 val ML_profiling_entryN = "ML_profiling_entry";
 fun ML_profiling_entry {name, count} =
   (ML_profiling_entryN, [(nameN, name), (countN, Value.print_int count)]);
 
 val (ML_profilingN, ML_profiling) = markup_string "ML_profiling" kindN;
 
 
 (* 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 function name = ("function", name);
 
 fun ML_statistics {pid, stats_dir} =
-  [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)];
-
-val commands_accepted = [(functionN, "commands_accepted")];
-
-val assign_update = [(functionN, "assign_update")];
-val removed_versions = [(functionN, "removed_versions")];
-
-fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
-
-fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
+  [function "ML_statistics", ("pid", Value.print_int pid), ("stats_dir", stats_dir)];
 
-val task_statistics = (functionN, "task_statistics");
-
-val command_timing = (functionN, "command_timing");
-
-val theory_timing = (functionN, "theory_timing");
+val commands_accepted = [function "commands_accepted"];
 
-val session_timing = (functionN, "session_timing");
+val assign_update = [function "assign_update"];
+val removed_versions = [function "removed_versions"];
 
-fun loading_theory name = [(functionN, "loading_theory"), (nameN, name)];
+fun invoke_scala name id = [function "invoke_scala", (nameN, name), (idN, id)];
 
-val build_session_finished = [(functionN, "build_session_finished")];
+fun cancel_scala id = [function "cancel_scala", (idN, id)];
 
-val print_operations = [(functionN, "print_operations")];
+val task_statistics = function "task_statistics";
+
+val command_timing = function "command_timing";
+
+val theory_timing = function "theory_timing";
+
+val session_timing = function "session_timing";
+
+fun loading_theory name = [function "loading_theory", (nameN, name)];
+
+val build_session_finished = [function "build_session_finished"];
+
+val print_operations = [function "print_operations"];
 
 
 (* 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),
+ [function 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)];
+fun debugger_state name = [function "debugger_state", (nameN, name)];
+fun debugger_output name = [function "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)];
+fun simp_trace_cancel i = [function "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,758 +1,758 @@
 /*  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_Elem(val name: String) {
     def apply(props: Properties.T = Nil): Markup = Markup(name, props)
     def unapply(markup: Markup): Option[Properties.T] =
       if (markup.name == name) Some(markup.properties) else None
   }
 
   class Markup_String(val name: String, prop: String) {
     val Prop: Properties.String = 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
     def get(markup: Markup): String = unapply(markup).getOrElse("")
   }
 
   class Markup_Int(val name: String, prop: String) {
     val Prop: Properties.Int = 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
     def get(markup: Markup): Int = unapply(markup).getOrElse(0)
   }
 
   class Markup_Long(val name: String, prop: String) {
     val Prop: Properties.Long = 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
     def get(markup: Markup): Long = unapply(markup).getOrElse(0)
   }
 
 
   /* 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 Markup_Long(ENTITY, "def")
     val Ref = new Markup_Long(ENTITY, "ref")
 
     object Occ {
       def unapply(markup: Markup): Option[Long] =
         Def.unapply(markup) orElse Ref.unapply(markup)
     }
 
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) => Some((Kind.get(props), Name.get(props)))
         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 = "position"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
 
   /* position "def" name */
 
   private val def_names: Map[String, String] =
     Map(LINE -> DEF_LINE, OFFSET -> DEF_OFFSET, END_OFFSET -> DEF_END_OFFSET,
       FILE -> DEF_FILE, ID -> DEF_ID)
 
   def def_name(a: String): String = def_names.getOrElse(a, a + "def_")
 
 
   /* expression */
 
   val EXPRESSION = "expression"
   object Expression {
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(EXPRESSION, props) => Some(Kind.get(props))
         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
       }
 
     object Path {
       def unapply(markup: Markup): Option[Boolean] =
         markup match {
           case Language(PATH, _, _, delimited) => Some(delimited)
           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.get(markup.properties)
         val i = Indent.get(markup.properties)
         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.get(markup.properties)
         val i = Indent.get(markup.properties)
         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 SESSION = "session"
 
   val THEORY = "theory"
   val CLASS = "class"
   val LOCALE = "locale"
   val BUNDLE = "bundle"
   val TYPE_NAME = "type_name"
   val CONSTANT = "constant"
   val AXIOM = "axiom"
   val FACT = "fact"
   val ORACLE = "oracle"
 
   val FIXED = "fixed"
   val CASE = "case"
   val DYNAMIC_FACT = "dynamic_fact"
   val LITERAL_FACT = "literal_fact"
 
   val ATTRIBUTE = "attribute"
   val METHOD = "method"
   val METHOD_MODIFIER = "method_modifier"
 
 
   /* 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"
 
 
   /* 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 extends Markup_String("document_tag", NAME) {
     val IMPORTANT = "important"
     val UNIMPORTANT = "unimportant"
   }
 
 
   /* LaTeX */
 
   val Document_Latex = new Markup_Elem("document_latex")
 
   val Latex_Output = new Markup_Elem("latex_output")
   val Latex_Macro0 = new Markup_String("latex_macro0", NAME)
   val Latex_Macro = new Markup_String("latex_macro", NAME)
   val Latex_Environment = new Markup_String("latex_environment", NAME)
   val Latex_Heading = new Markup_String("latex_heading", KIND)
   val Latex_Body = new Markup_String("latex_body", KIND)
   val Latex_Delim = new Markup_String("latex_delim", NAME)
   val Latex_Tag = new Markup_String("latex_tag", NAME)
 
   val Latex_Index_Item = new Markup_Elem("latex_index_item")
   val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)
 
   val Optional_Argument = new Properties.String("optional_argument")
 
 
   /* 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_SPAN = "command_span"
   val Command_Span = new Markup_String(COMMAND_SPAN, NAME)
 
   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 CARTOUCHE = "cartouche"
   val COMMENT = "comment"
 
   val LOAD_COMMAND = "load_command"
 
 
   /* 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 get(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 */
 
   val Command_Indent = new Markup_Int("command_indent", Indent.name)
 
 
   /* 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"
 
 
   /* ML profiling */
 
   val COUNT = "count"
   val ML_PROFILING_ENTRY = "ML_profiling_entry"
   val ML_PROFILING = "ML_profiling"
 
   object ML_Profiling {
     def unapply_entry(tree: XML.Tree): Option[isabelle.ML_Profiling.Entry] =
       tree match {
         case XML.Elem(Markup(ML_PROFILING_ENTRY, List((NAME, name), (COUNT, Value.Long(count)))), _) =>
           Some(isabelle.ML_Profiling.Entry(name, count))
         case _ => None
       }
 
     def unapply_report(tree: XML.Tree): Option[isabelle.ML_Profiling.Report] =
       tree match {
         case XML.Elem(Markup(ML_PROFILING, List((KIND, kind))), body) =>
           Some(isabelle.ML_Profiling.Report(kind, body.flatMap(unapply_entry)))
         case _ => None
       }
   }
 
 
   /* 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)
+    val THIS: 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 THIS :: 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 List(THIS, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
   object ML_Statistics extends Function("ML_statistics") {
     def unapply(props: Properties.T): Option[(Long, String)] =
       props match {
-        case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
+        case List(THIS, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
           Some((pid, stats_dir))
         case _ => None
       }
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   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 Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Properties_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
   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 List(THIS, (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 List(THIS, (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 is_empty: Boolean = name.isEmpty
 
   def position_properties: Position.T = properties.filter(Markup.position_property)
 
   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.foldRight(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,751 +1,751 @@
 /*  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]): Unit = consumers.change(Library.update(c))
     def -= (c: Consumer[A]): Unit = consumers.change(Library.remove(c))
 
     def post(a: A): Unit = {
       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 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
   type Protocol_Functions = List[(String, Protocol_Function)]
 
   abstract class Protocol_Handler extends Isabelle_System.Service {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
     def functions: Protocol_Functions = Nil
     def prover_options(options: Options): Options = options
   }
 }
 
 
 class Session(_session_options: => Options, val resources: Resources) extends Document.Session {
   session =>
 
   val cache: Term.Cache = Term.Cache.make()
 
   def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
     Command.Blobs_Info.none
 
 
   /* 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(), "not on dispatcher 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 finished_theories = new Session.Outlet[Document.Snapshot](dispatcher)
   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_Raw(name: String, args: List[Bytes])
   private case class Protocol_Command_Args(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(more_nodes = 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(): Unit = {
       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(): Unit = {
       delay.revoke()
       state.change(_ => None)
     }
 
     def update(more_nodes: Set[Document.Node.Name] = Set.empty): Unit = {
       val active =
         state.change_result(st =>
           (st.isDefined, st.map(nodes => if (nodes.isEmpty) more_nodes else nodes ++ more_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): Unit = variable.change(_ => Some(p))
     def reset(): Unit = variable.change(_ => None)
     def await_reset(): Unit = variable.guarded_access({ case None => Some((), None) case _ => None })
   }
 
 
   /* file formats and protocol handlers */
 
   private lazy val file_formats: File_Format.Session =
     File_Format.registry.start_session(session)
 
   private val protocol_handlers = Protocol_Handlers.init(session)
 
   def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] =
     protocol_handlers.get(c.getName) match {
       case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C])
       case _ => None
     }
 
   def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
     protocol_handlers.init(handler)
 
   def prover_options(options: Options): Options =
     protocol_handlers.prover_options(file_formats.prover_options(options))
 
 
   /* 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): Unit = {
     //{{{
       require(prover.defined, "prover process not defined (handle_raw_edits)")
 
       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): Unit = {
     //{{{
       require(prover.defined, "prover process not defined (handle_change)")
 
       // define commands
       {
         val id_commands = new mutable.ListBuffer[Command]
         def id_command(command: Command): Unit = {
           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(resources, 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): Unit = {
     //{{{
       def bad_output(): Unit = {
         if (verbose)
           Output.warning("Ignoring bad prover output: " + output.message.toString)
       }
 
       def change_command(f: Document.State => (Command.State, Document.State)): Unit = {
         try {
           val st = global_state.change_result(f)
           if (!st.command.span.is_theory) {
             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 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, cache.elem(message), cache))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(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 entry = Export.make_entry(Sessions.DRAFT, args, msg.chunk, cache)
                 change_command(_.add_export(id, (args.serial, entry)))
 
               case Protocol.Loading_Theory(node_name, id) =>
                 val blobs_info = build_blobs_info(node_name)
                 try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) }
                 catch { case _: Document.State.Fail => bad_output() }
 
-              case List(Markup.Commands_Accepted.PROPERTY) =>
+              case List(Markup.Commands_Accepted.THIS) =>
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
                     ids.foreach(id =>
                       change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache)))
                   case _ => bad_output()
                 }
 
-              case List(Markup.Assign_Update.PROPERTY) =>
+              case List(Markup.Assign_Update.THIS) =>
                 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) =>
+              case List(Markup.Removed_Versions.THIS) =>
                 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, cache))
 
             case _ if output.is_init =>
               val init_ok =
                 try {
                   Isabelle_System.make_services(classOf[Session.Protocol_Handler])
                     .foreach(init_protocol_handler)
                   true
                 }
                 catch {
                   case exn: Throwable =>
                     prover.get.protocol_command("Prover.stop", "1", Exn.message(exn))
                     false
                 }
 
               if (init_ok) {
                 prover.get.options(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()
               for (id <- global_state.value.theories.keys) {
                 val snapshot = global_state.change_result(_.end_theory(id))
                 finished_theories.post(snapshot)
               }
               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(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_Raw(name, args) if prover.defined =>
             prover.get.protocol_command_raw(name, args)
 
           case Protocol_Command_Args(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): Unit = {
     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_raw(name: String, args: List[Bytes]): Unit =
     manager.send(Protocol_Command_Raw(name, args))
 
   def protocol_command_args(name: String, args: List[String]): Unit =
     manager.send(Protocol_Command_Args(name, args))
 
   def protocol_command(name: String, args: String*): Unit =
     protocol_command_args(name, args.toList)
 
   def cancel_exec(exec_id: Document_ID.Exec): Unit =
     manager.send(Cancel_Exec(exec_id))
 
   def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Unit =
     if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits))
 
   def update_options(options: Options): Unit =
     manager.send_wait(Update_Options(options))
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String): Unit =
     manager.send(Session.Dialog_Result(id, serial, result))
 }