diff --git a/src/Pure/General/position.ML b/src/Pure/General/position.ML
--- a/src/Pure/General/position.ML
+++ b/src/Pure/General/position.ML
@@ -1,306 +1,306 @@
 (*  Title:      Pure/General/position.ML
     Author:     Makarius
 
 Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
 symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
 right-open interval offset .. end_offset (exclusive).
 *)
 
 signature POSITION =
 sig
   eqtype T
   val ord: T ord
   val make: Thread_Position.T -> T
   val dest: T -> Thread_Position.T
   val line_of: T -> int option
   val offset_of: T -> int option
   val end_offset_of: T -> int option
   val file_of: T -> string option
   val id_of: T -> string option
   val symbol: Symbol.symbol -> T -> T
   val symbol_explode: string -> T -> T
   val distance_of: T * T -> int option
   val none: T
   val start: T
   val file_name: string -> Properties.T
   val file_only: string -> T
   val file: string -> T
   val line_file_only: int -> string -> T
   val line_file: int -> string -> T
   val line: int -> T
   val get_props: T -> Properties.T
   val id: string -> T
   val id_only: string -> T
   val put_id: string -> T -> T
   val copy_id: T -> T -> T
   val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
   val advance_offsets: int -> T -> T
   val adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val offset_properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
   val entity_properties_of: bool -> serial -> T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
   val is_reported_range: T -> bool
   val reported_text: T -> Markup.T -> string -> string
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
   type report = T * Markup.T
   type report_text = report * string
   val reports_text: report_text list -> unit
   val reports: report list -> unit
   val store_reports: report_text list Unsynchronized.ref ->
     T list -> ('a -> Markup.T list) -> 'a -> unit
   val append_reports: report_text list Unsynchronized.ref -> report list -> unit
   val here_strs: T -> string * string
   val here: T -> string
   val here_list: T list -> string
   type range = T * T
   val no_range: range
   val no_range_position: T -> T
   val range_position: range -> T
   val range: T * T -> range
   val range_of_properties: Properties.T -> range
   val properties_of_range: range -> Properties.T
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
   val default: T -> bool * T
 end;
 
 structure Position: POSITION =
 struct
 
 (* datatype position *)
 
 type count = int * int * int;
 datatype T = Pos of count * Properties.T;
 
 fun dest2 f = apply2 (fn Pos p => f p);
 
 val ord =
   pointer_eq_ord
    (int_ord o dest2 (#1 o #1) |||
     int_ord o dest2 (#2 o #1) |||
     int_ord o dest2 (#3 o #1) |||
     Properties.ord o dest2 #2);
 
 fun norm_props (props: Properties.T) =
   maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
     [Markup.fileN, Markup.idN];
 
 fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
 
 fun valid (i: int) = i > 0;
 val invalid = not o valid;
 fun maybe_valid i = if valid i then SOME i else NONE;
 fun if_valid i i' = if valid i then i' else i;
 
 
 (* fields *)
 
 fun line_of (Pos ((i, _, _), _)) = maybe_valid i;
 fun offset_of (Pos ((_, j, _), _)) = maybe_valid j;
 fun end_offset_of (Pos ((_, _, k), _)) = maybe_valid k;
 
 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
 fun id_of (Pos (_, props)) = Properties.get props Markup.idN;
 
 
 (* count position *)
 
 fun count_symbol "\n" ((i, j, k): count) =
       (if_valid i (i + 1), if_valid j (j + 1), k)
   | count_symbol s (i, j, k) =
       if Symbol.not_eof s then (i, if_valid j (j + 1), k) else (i, j, k);
 
 fun count_invalid ((i, j, _): count) = invalid i andalso invalid j;
 
 fun symbol sym (pos as (Pos (count, props))) =
   if count_invalid count then pos else Pos (count_symbol sym count, props);
 
 val symbol_explode = fold symbol o Symbol.explode;
 
 
 (* distance of adjacent positions *)
 
 fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
   if valid j andalso valid j' then SOME (j' - j) else NONE;
 
 
 (* make position *)
 
 val none = Pos ((0, 0, 0), []);
 val start = Pos ((1, 1, 0), []);
 
 
 fun file_name "" = []
   | file_name name = [(Markup.fileN, name)];
 
 fun file_only name = Pos ((0, 0, 0), file_name name);
 fun file name = Pos ((1, 1, 0), file_name name);
 
 fun line_file_only i name = Pos ((i, 0, 0), file_name name);
 fun line_file i name = Pos ((i, 1, 0), file_name name);
 fun line i = line_file i "";
 
 fun get_props (Pos (_, props)) = props;
 
 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
 
 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
 fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
 
 fun parse_id pos = Option.map Value.parse_int (id_of pos);
 
 fun id_properties_of pos =
   (case id_of pos of
     SOME id => [(Markup.idN, id)]
   | NONE => []);
 
 
 (* adjust offsets *)
 
 fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
   if offset = 0 orelse count_invalid count then pos
   else if offset < 0 then raise Fail "Illegal offset"
   else if valid i then raise Fail "Illegal line position"
   else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
 
 fun adjust_offsets adjust (pos as Pos (_, props)) =
   if is_none (file_of pos) then
     (case parse_id pos of
       SOME id =>
         (case adjust id of
           SOME offset =>
             let val Pos (count, _) = advance_offsets offset pos
             in Pos (count, Properties.remove Markup.idN props) end
         | NONE => pos)
     | NONE => pos)
   else pos;
 
 
 (* markup properties *)
 
 fun get_int props name =
   (case Properties.get props name of
     NONE => 0
   | SOME s => Value.parse_int s);
 
 fun of_properties props =
   make {
     line = get_int props Markup.lineN,
     offset = get_int props Markup.offsetN,
     end_offset = get_int props Markup.end_offsetN,
     props = props};
 
 fun int_entry k i = if invalid i then [] else [(k, Value.print_int i)];
 
 fun properties_of (Pos ((i, j, k), props)) =
   int_entry Markup.lineN i @
   int_entry Markup.offsetN j @
   int_entry Markup.end_offsetN k @ props;
 
 fun offset_properties_of (Pos ((_, j, k), _)) =
   int_entry Markup.offsetN j @
   int_entry Markup.end_offsetN k;
 
-val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
+val def_properties_of = properties_of #> map (apfst Markup.def_name);
 
 fun entity_markup kind (name, pos) =
   Markup.entity kind name |> Markup.properties (def_properties_of pos);
 
 fun entity_properties_of def serial pos =
   if def then (Markup.defN, Value.print_int serial) :: properties_of pos
   else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
 
 val markup = Markup.properties o properties_of;
 
 
 (* reports *)
 
 fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos);
 fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
 
 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
 fun report_text pos markup txt = Output.report [reported_text pos markup txt];
 fun report pos markup = report_text pos markup "";
 
 type report = T * Markup.T;
 type report_text = report * string;
 
 val reports_text =
   map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
   #> Output.report;
 
 val reports = map (rpair "") #> reports_text;
 
 fun store_reports _ [] _ _ = ()
   | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
 
 fun append_reports (r: report_text list Unsynchronized.ref) reports =
   Unsynchronized.change r (append (map (rpair "") reports));
 
 
 (* here: user output *)
 
 fun here_strs pos =
   (case (line_of pos, file_of pos) of
     (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
   | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
   | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
   | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
 
 fun here pos =
   let
     val props = properties_of pos;
     val (s1, s2) = here_strs pos;
   in
     if s2 = "" then ""
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;
 
 val here_list = map here #> distinct (op =) #> implode;
 
 
 (* range *)
 
 type range = T * T;
 
 val no_range = (none, none);
 
 fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
 fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
 fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
 
 fun range_of_properties props =
   let
     val pos = of_properties props;
     val pos' =
       make {line = get_int props Markup.end_lineN,
         offset = get_int props Markup.end_offsetN,
         end_offset = 0,
         props = props};
   in (pos, pos') end;
 
 fun properties_of_range (pos, pos') =
   properties_of pos @ int_entry Markup.end_lineN (the_default 0 (line_of pos'));
 
 
 (* thread data *)
 
 val thread_data = make o Thread_Position.get;
 fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
 
 fun default pos =
   if pos = none then (false, thread_data ())
   else (true, pos);
 
 end;
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,816 +1,829 @@
 (*  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 positionN: string val position: T
+  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 bash_functionN: string
   val scala_functionN: string
   val system_optionN: string
   val sessionN: string
   val theoryN: string
   val classN: string
   val localeN: 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 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 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 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_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};
 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);
 
-val (positionN, position) = markup_elem "position";
+
+(* 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 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 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;
 
 val (document_latexN, document_latex) = markup_elem "document_latex";
 
 
 (* 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";
 
 
 (* 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 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)];
 
 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"), (nameN, 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,776 +1,785 @@
 /*  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"
 
   val Def = new Properties.Long("def")
   val Ref = new Properties.Long("ref")
 
   object Entity
   {
     object Def
     {
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None
     }
     object Ref
     {
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
     }
     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) =>
           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 = "position"
+
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
-  val POSITION = "position"
+
+  /* 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, 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
       }
 
     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.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 SESSION = "session"
 
   val THEORY = "theory"
   val CLASS = "class"
   val LOCALE = "locale"
   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
   {
     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
       }
   }
 
   val DOCUMENT_LATEX = "document_latex"
 
 
   /* 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"
 
   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 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"
 
 
   /* 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)
   }
 
   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_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)) =>
           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 _ => 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 is_empty: Boolean = name.isEmpty
 
   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/Tools/Haskell/Haskell.thy b/src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy
+++ b/src/Tools/Haskell/Haskell.thy
@@ -1,3532 +1,3554 @@
 (*  Title:      Tools/Haskell/Haskell.thy
     Author:     Makarius
 
 Support for Isabelle tools in Haskell.
 *)
 
 theory Haskell
   imports Main
 begin
 
 generate_file "Isabelle/Bytes.hs" = \<open>
 {-  Title:      Isabelle/Bytes.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Compact byte strings.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/bytes.ML\<close>
 and \<^file>\<open>$ISABELLE_HOME/src/Pure/General/bytes.scala\<close>.
 -}
 
 {-# LANGUAGE TypeApplications #-}
 
 module Isabelle.Bytes (
   Bytes,
   make, unmake, pack, unpack,
   empty, null, length, index, all, any,
   head, last, take, drop, isPrefixOf, isSuffixOf,
   concat, space, spaces, char, all_char, any_char, byte, singleton
 )
 where
 
 import Prelude hiding (null, length, all, any, head, last, take, drop, concat)
 
 import qualified Data.ByteString.Short as ShortByteString
 import Data.ByteString.Short (ShortByteString)
 import qualified Data.ByteString as ByteString
 import Data.ByteString (ByteString)
 import qualified Data.List as List
 import Data.Word (Word8)
 import Data.Array (Array, array, (!))
 
 
 type Bytes = ShortByteString
 
 make :: ByteString -> Bytes
 make = ShortByteString.toShort
 
 unmake :: Bytes -> ByteString
 unmake = ShortByteString.fromShort
 
 pack :: [Word8] -> Bytes
 pack = ShortByteString.pack
 
 unpack :: Bytes -> [Word8]
 unpack = ShortByteString.unpack
 
 empty :: Bytes
 empty = ShortByteString.empty
 
 null :: Bytes -> Bool
 null = ShortByteString.null
 
 length :: Bytes -> Int
 length = ShortByteString.length
 
 index :: Bytes -> Int -> Word8
 index = ShortByteString.index
 
 all :: (Word8 -> Bool) -> Bytes -> Bool
 all p = List.all p . unpack
 
 any :: (Word8 -> Bool) -> Bytes -> Bool
 any p = List.any p . unpack
 
 head :: Bytes -> Word8
 head bytes = index bytes 0
 
 last :: Bytes -> Word8
 last bytes = index bytes (length bytes - 1)
 
 take :: Int -> Bytes -> Bytes
 take n = pack . List.take n . unpack
 
 drop :: Int -> Bytes -> Bytes
 drop n = pack . List.drop n . unpack
 
 isPrefixOf :: Bytes -> Bytes -> Bool
 isPrefixOf bs1 bs2 =
   n1 <= n2 && List.all (\i -> index bs1 i == index bs2 i) [0 .. n1 - 1]
   where n1 = length bs1; n2 = length bs2
 
 isSuffixOf :: Bytes -> Bytes -> Bool
 isSuffixOf bs1 bs2 =
   n1 <= n2 && List.all (\i -> index bs1 i == index bs2 (i + k)) [0 .. n1 - 1]
   where n1 = length bs1; n2 = length bs2; k = n2 - n1
 
 concat :: [Bytes] -> Bytes
 concat = mconcat
 
 space :: Word8
 space = 32
 
 small_spaces :: Array Int Bytes
 small_spaces = array (0, 64) [(i, pack (replicate i space)) | i <- [0 .. 64]]
 
 spaces :: Int -> Bytes
 spaces n =
   if n < 64 then small_spaces ! n
   else concat ((small_spaces ! (n `mod` 64)) : replicate (n `div` 64) (small_spaces ! 64))
 
 char :: Word8 -> Char
 char = toEnum . fromEnum
 
 all_char :: (Char -> Bool) -> Bytes -> Bool
 all_char pred = all (pred . char)
 
 any_char :: (Char -> Bool) -> Bytes -> Bool
 any_char pred = any (pred . char)
 
 byte :: Char -> Word8
 byte = toEnum . fromEnum
 
 singletons :: Array Word8 Bytes
 singletons =
   array (minBound, maxBound)
     [(i, make (ByteString.singleton i)) | i <- [minBound .. maxBound]]
 
 singleton :: Word8 -> Bytes
 singleton b = singletons ! b
 \<close>
 
 generate_file "Isabelle/UTF8.hs" = \<open>
 {-  Title:      Isabelle/UTF8.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Variations on UTF-8.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/utf8.ML\<close>
 and \<^file>\<open>$ISABELLE_HOME/src/Pure/General/utf8.scala\<close>.
 -}
 
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE InstanceSigs #-}
 
 module Isabelle.UTF8 (
   setup, setup3,
   Recode (..)
 )
 where
 
 import qualified System.IO as IO
 import Data.Text (Text)
 import qualified Data.Text as Text
 import qualified Data.Text.Encoding as Encoding
 import qualified Data.Text.Encoding.Error as Error
 
 import Data.ByteString (ByteString)
 
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 
 setup :: IO.Handle -> IO ()
 setup h = do
   IO.hSetEncoding h IO.utf8
   IO.hSetNewlineMode h IO.noNewlineTranslation
 
 setup3 :: IO.Handle -> IO.Handle -> IO.Handle -> IO ()
 setup3 h1 h2 h3 = do
   setup h1
   setup h2
   setup h3
 
 class Recode a b where
   encode :: a -> b
   decode :: b -> a
 
 instance Recode Text ByteString where
   encode :: Text -> ByteString
   encode = Encoding.encodeUtf8
   decode :: ByteString -> Text
   decode = Encoding.decodeUtf8With Error.lenientDecode
 
 instance Recode Text Bytes where
   encode :: Text -> Bytes
   encode = Bytes.make . encode
   decode :: Bytes -> Text
   decode = decode . Bytes.unmake
 
 instance Recode String ByteString where
   encode :: String -> ByteString
   encode = encode . Text.pack
   decode :: ByteString -> String
   decode = Text.unpack . decode
 
 instance Recode String Bytes where
   encode :: String -> Bytes
   encode = encode . Text.pack
   decode :: Bytes -> String
   decode = Text.unpack . decode
 \<close>
 
 generate_file "Isabelle/Library.hs" = \<open>
 {-  Title:      Isabelle/Library.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Basic library of Isabelle idioms.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>
 and \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE InstanceSigs #-}
 
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
 
   fold, fold_rev, single, map_index, get_index, separate,
 
   StringLike, STRING (..), TEXT (..), BYTES (..),
   show_bytes, show_text,
 
   proper_string, quote, space_implode, commas, commas_quote, cat_lines,
   space_explode, split_lines, trim_line)
 where
 
 import qualified Data.Text as Text
 import Data.Text (Text)
 import qualified Data.Text.Lazy as Lazy
 import Data.String (IsString)
 import qualified Data.List.Split as Split
 import qualified Isabelle.Symbol as Symbol
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.UTF8 as UTF8
 
 
 {- functions -}
 
 (|>) :: a -> (a -> b) -> b
 x |> f = f x
 
 (|->) :: (a, b) -> (a -> b -> c) -> c
 (x, y) |-> f = f x y
 
 (#>) :: (a -> b) -> (b -> c) -> a -> c
 (f #> g) x = x |> f |> g
 
 (#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
 (f #-> g) x  = x |> f |-> g
 
 
 {- lists -}
 
 fold :: (a -> b -> b) -> [a] -> b -> b
 fold _ [] y = y
 fold f (x : xs) y = fold f xs (f x y)
 
 fold_rev :: (a -> b -> b) -> [a] -> b -> b
 fold_rev _ [] y = y
 fold_rev f (x : xs) y = f x (fold_rev f xs y)
 
 single :: a -> [a]
 single x = [x]
 
 map_index :: ((Int, a) -> b) -> [a] -> [b]
 map_index f = map_aux 0
   where
     map_aux _ [] = []
     map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
 
 get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
 get_index f = get_aux 0
   where
     get_aux _ [] = Nothing
     get_aux i (x : xs) =
       case f x of
         Nothing -> get_aux (i + 1) xs
         Just y -> Just (i, y)
 
 separate :: a -> [a] -> [a]
 separate s (x : (xs @ (_ : _))) = x : s : separate s xs
 separate _ xs = xs;
 
 
 {- string-like interfaces -}
 
 class (IsString a, Monoid a, Eq a, Ord a) => StringLike a where
   space_explode :: Char -> a -> [a]
   trim_line :: a -> a
 
 gen_trim_line :: Int -> (Int -> Char) -> (Int -> a -> a) -> a -> a
 gen_trim_line n at trim s =
   if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then trim (n - 2) s
   else if n >= 1 && Symbol.is_ascii_line_terminator (at (n - 1)) then trim (n - 1) s
   else s
 
 instance StringLike String where
   space_explode :: Char -> String -> [String]
   space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
   trim_line :: String -> String
   trim_line s = gen_trim_line (length s) ((!!) s) take s
 
 instance StringLike Text where
   space_explode :: Char -> Text -> [Text]
   space_explode c str =
     if Text.null str then []
     else if Text.all (/= c) str then [str]
     else map Text.pack $ space_explode c $ Text.unpack str
   trim_line :: Text -> Text
   trim_line s = gen_trim_line (Text.length s) (Text.index s) Text.take s
 
 instance StringLike Lazy.Text where
   space_explode :: Char -> Lazy.Text -> [Lazy.Text]
   space_explode c str =
     if Lazy.null str then []
     else if Lazy.all (/= c) str then [str]
     else map Lazy.pack $ space_explode c $ Lazy.unpack str
   trim_line :: Lazy.Text -> Lazy.Text
   trim_line = Lazy.fromStrict . trim_line . Lazy.toStrict
 
 instance StringLike Bytes where
   space_explode :: Char -> Bytes -> [Bytes]
   space_explode c str =
     if Bytes.null str then []
     else if Bytes.all_char (/= c) str then [str]
     else
       explode (Bytes.unpack str)
       where
         explode rest =
           case span (/= (Bytes.byte c)) rest of
             (_, []) -> [Bytes.pack rest]
             (prfx, _ : rest') -> Bytes.pack prfx : explode rest'
   trim_line :: Bytes -> Bytes
   trim_line s = gen_trim_line (Bytes.length s) (Bytes.char . Bytes.index s) Bytes.take s
 
 class StringLike a => STRING a where make_string :: a -> String
 instance STRING String where make_string = id
 instance STRING Text where make_string = Text.unpack
 instance STRING Lazy.Text where make_string = Lazy.unpack
 instance STRING Bytes where make_string = UTF8.decode
 
 class StringLike a => TEXT a where make_text :: a -> Text
 instance TEXT String where make_text = Text.pack
 instance TEXT Text where make_text = id
 instance TEXT Lazy.Text where make_text = Lazy.toStrict
 instance TEXT Bytes where make_text = UTF8.decode
 
 class StringLike a => BYTES a where make_bytes :: a -> Bytes
 instance BYTES String where make_bytes = UTF8.encode
 instance BYTES Text where make_bytes = UTF8.encode
 instance BYTES Lazy.Text where make_bytes = UTF8.encode . Lazy.toStrict
 instance BYTES Bytes where make_bytes = id
 
 show_bytes :: Show a => a -> Bytes
 show_bytes = make_bytes . show
 
 show_text :: Show a => a -> Text
 show_text = make_text . show
 
 
 {- strings -}
 
 proper_string :: StringLike a => a -> Maybe a
 proper_string s = if s == "" then Nothing else Just s
 
 quote :: StringLike a => a -> a
 quote s = "\"" <> s <> "\""
 
 space_implode :: StringLike a => a -> [a] -> a
 space_implode s = mconcat . separate s
 
 commas, commas_quote :: StringLike a => [a] -> a
 commas = space_implode ", "
 commas_quote = commas . map quote
 
 split_lines :: StringLike a => a -> [a]
 split_lines = space_explode '\n'
 
 cat_lines :: StringLike a => [a] -> a
 cat_lines = space_implode "\n"
 \<close>
 
 
 generate_file "Isabelle/Symbol.hs" = \<open>
 {-  Title:      Isabelle/Symbols.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Isabelle text symbols.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/symbol.ML\<close>
 and \<^file>\<open>$ISABELLE_HOME/src/Pure/General/symbol_explode.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Symbol (
   Symbol, eof, is_eof, not_eof,
 
   is_ascii_letter, is_ascii_digit, is_ascii_hex, is_ascii_quasi,
   is_ascii_blank, is_ascii_line_terminator, is_ascii_letdig,
   is_ascii_identifier,
 
   explode
 )
 where
 
 import Data.Word (Word8)
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 
 
 {- type -}
 
 type Symbol = Bytes
 
 eof :: Symbol
 eof = ""
 
 is_eof, not_eof :: Symbol -> Bool
 is_eof = Bytes.null
 not_eof = not . is_eof
 
 
 {- ASCII characters -}
 
 is_ascii_letter :: Char -> Bool
 is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
 
 is_ascii_digit :: Char -> Bool
 is_ascii_digit c = '0' <= c && c <= '9'
 
 is_ascii_hex :: Char -> Bool
 is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
 
 is_ascii_quasi :: Char -> Bool
 is_ascii_quasi c = c == '_' || c == '\''
 
 is_ascii_blank :: Char -> Bool
 is_ascii_blank c = c `elem` (" \t\n\11\f\r" :: String)
 
 is_ascii_line_terminator :: Char -> Bool
 is_ascii_line_terminator c = c == '\r' || c == '\n'
 
 is_ascii_letdig :: Char -> Bool
 is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c
 
 is_ascii_identifier :: String -> Bool
 is_ascii_identifier s =
   not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
 
 
 {- explode symbols: ASCII, UTF8, named -}
 
 is_utf8 :: Word8 -> Bool
 is_utf8 b = b >= 128
 
 is_utf8_trailer :: Word8 -> Bool
 is_utf8_trailer b = 128 <= b && b < 192
 
 is_utf8_control :: Word8 -> Bool
 is_utf8_control b = 128 <= b && b < 160
 
 (|>) :: a -> (a -> b) -> b
 x |> f = f x
 
 explode :: Bytes -> [Symbol]
 explode string = scan 0
   where
     byte = Bytes.index string
     substring i j =
       if i == j - 1 then Bytes.singleton (byte i)
       else Bytes.pack (map byte [i .. j - 1])
 
     n = Bytes.length string
     test pred i = i < n && pred (byte i)
     test_char pred i = i < n && pred (Bytes.char (byte i))
     many pred i = if test pred i then many pred (i + 1) else i
     maybe_char c i = if test_char (== c) i then i + 1 else i
     maybe_ascii_id i =
       if test_char is_ascii_letter i
       then many (is_ascii_letdig . Bytes.char) (i + 1)
       else i
 
     scan i =
       if i < n then
         let
           b = byte i
           c = Bytes.char b
         in
           {-encoded newline-}
           if c == '\r' then "\n" : scan (maybe_char '\n' (i + 1))
           {-pseudo utf8: encoded ascii control-}
           else if b == 192 && test is_utf8_control (i + 1) && not (test is_utf8 (i + 2))
           then Bytes.singleton (byte (i + 1) - 128) : scan (i + 2)
           {-utf8-}
           else if is_utf8 b then
             let j = many is_utf8_trailer (i + 1)
             in substring i j : scan j
           {-named symbol-}
           else if c == '\\' && test_char (== '<') (i + 1) then
             let j = (i + 2) |> maybe_char '^' |> maybe_ascii_id |> maybe_char '>'
             in substring i j : scan j
           {-single character-}
           else Bytes.singleton b : scan (i + 1)
       else []
 \<close>
 
 generate_file "Isabelle/Buffer.hs" = \<open>
 {-  Title:      Isabelle/Buffer.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Efficient buffer of byte strings.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
 -}
 
 module Isabelle.Buffer (T, empty, add, content)
 where
 
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 
 
 newtype T = Buffer [Bytes]
 
 empty :: T
 empty = Buffer []
 
 add :: Bytes -> T -> T
 add b (Buffer bs) = Buffer (if Bytes.null b then bs else b : bs)
 
 content :: T -> Bytes
 content (Buffer bs) = Bytes.concat (reverse bs)
 \<close>
 
 generate_file "Isabelle/Value.hs" = \<open>
 {-  Title:      Isabelle/Value.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Plain values, represented as string.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/value.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Value
   (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real)
 where
 
 import qualified Data.List as List
 import qualified Text.Read as Read
 import Isabelle.Bytes (Bytes)
 import Isabelle.Library
 
 
 {- bool -}
 
 print_bool :: Bool -> Bytes
 print_bool True = "true"
 print_bool False = "false"
 
 parse_bool :: Bytes -> Maybe Bool
 parse_bool "true" = Just True
 parse_bool "false" = Just False
 parse_bool _ = Nothing
 
 
 {- nat -}
 
 parse_nat :: Bytes -> Maybe Int
 parse_nat s =
   case Read.readMaybe (make_string s) of
     Just n | n >= 0 -> Just n
     _ -> Nothing
 
 
 {- int -}
 
 print_int :: Int -> Bytes
 print_int = show_bytes
 
 parse_int :: Bytes -> Maybe Int
 parse_int = Read.readMaybe . make_string
 
 
 {- real -}
 
 print_real :: Double -> Bytes
 print_real x =
   let s = show x in
     case span (/= '.') s of
       (a, '.' : b) | List.all (== '0') b -> make_bytes a
       _ -> make_bytes s
 
 parse_real :: Bytes -> Maybe Double
 parse_real = Read.readMaybe . make_string
 \<close>
 
 generate_file "Isabelle/Properties.hs" = \<open>
 {-  Title:      Isabelle/Properties.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Property lists.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
 -}
 
 module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
 where
 
 import qualified Data.List as List
 import Isabelle.Bytes (Bytes)
 
 
 type Entry = (Bytes, Bytes)
 type T = [Entry]
 
 defined :: T -> Bytes -> Bool
 defined props name = any (\(a, _) -> a == name) props
 
 get :: T -> Bytes -> Maybe Bytes
 get props name = List.lookup name props
 
 get_value :: (Bytes -> Maybe a) -> T -> Bytes -> Maybe a
 get_value parse props name =
   case get props name of
     Nothing -> Nothing
     Just s -> parse s
 
 put :: Entry -> T -> T
 put entry props = entry : remove (fst entry) props
 
 remove :: Bytes -> T -> T
 remove name props =
   if defined props name then filter (\(a, _) -> a /= name) props
   else props
 \<close>
 
 generate_file "Isabelle/Markup.hs" = \<open>
 {-  Title:      Isabelle/Markup.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Quasi-abstract markup elements.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 
 module Isabelle.Markup (
   T, empty, is_empty, properties,
 
   nameN, name, xnameN, xname, kindN,
 
   bindingN, binding, entityN, entity, defN, refN,
 
   completionN, completion, no_completionN, no_completion,
 
   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
+  position_properties, def_name,
 
   expressionN, expression,
 
   citationN, citation,
 
   pathN, path, urlN, url, docN, doc,
 
   markupN, consistentN, unbreakableN, indentN, widthN,
   blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
 
   wordsN, words,
 
   tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
   numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
   inner_cartoucheN, inner_cartouche,
   token_rangeN, token_range,
   sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
 
   antiquotedN, antiquoted, antiquoteN, antiquote,
 
   paragraphN, paragraph, text_foldN, text_fold,
 
   keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
   improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
   verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
   comment2N, comment2, comment3N, comment3,
 
   forkedN, forked, joinedN, joined, runningN, running, finishedN, finished,
   failedN, failed, canceledN, canceled, initializedN, initialized, finalizedN, finalized,
   consolidatedN, consolidated,
 
   writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
   warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
 
   intensifyN, intensify,
   Output, no_output)
 where
 
 import Prelude hiding (words, error, break)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
 
 import Isabelle.Library
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Value as Value
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 
 
 {- basic markup -}
 
 type T = (Bytes, Properties.T)
 
 empty :: T
 empty = ("", [])
 
 is_empty :: T -> Bool
 is_empty ("", _) = True
 is_empty _ = False
 
 properties :: Properties.T -> T -> T
 properties more_props (elem, props) =
   (elem, fold_rev Properties.put more_props props)
 
 markup_elem :: Bytes -> T
 markup_elem name = (name, [])
 
 markup_string :: Bytes -> Bytes -> Bytes -> T
 markup_string name prop = \s -> (name, [(prop, s)])
 
 
 {- misc properties -}
 
 nameN :: Bytes
 nameN = \<open>Markup.nameN\<close>
 
 name :: Bytes -> T -> T
 name a = properties [(nameN, a)]
 
 xnameN :: Bytes
 xnameN = \<open>Markup.xnameN\<close>
 
 xname :: Bytes -> T -> T
 xname a = properties [(xnameN, a)]
 
 kindN :: Bytes
 kindN = \<open>Markup.kindN\<close>
 
 
 {- formal entities -}
 
 bindingN :: Bytes
 bindingN = \<open>Markup.bindingN\<close>
 binding :: T
 binding = markup_elem bindingN
 
 entityN :: Bytes
 entityN = \<open>Markup.entityN\<close>
 entity :: Bytes -> Bytes -> T
 entity kind name =
   (entityN,
     (if Bytes.null name then [] else [(nameN, name)]) <>
     (if Bytes.null kind then [] else [(kindN, kind)]))
 
 defN :: Bytes
 defN = \<open>Markup.defN\<close>
 
 refN :: Bytes
 refN = \<open>Markup.refN\<close>
 
 
 {- completion -}
 
 completionN :: Bytes
 completionN = \<open>Markup.completionN\<close>
 completion :: T
 completion = markup_elem completionN
 
 no_completionN :: Bytes
 no_completionN = \<open>Markup.no_completionN\<close>
 no_completion :: T
 no_completion = markup_elem no_completionN
 
 
 {- position -}
 
 lineN, end_lineN :: Bytes
 lineN = \<open>Markup.lineN\<close>
 end_lineN = \<open>Markup.end_lineN\<close>
 
 offsetN, end_offsetN :: Bytes
 offsetN = \<open>Markup.offsetN\<close>
 end_offsetN = \<open>Markup.end_offsetN\<close>
 
 fileN, idN :: Bytes
 fileN = \<open>Markup.fileN\<close>
 idN = \<open>Markup.idN\<close>
 
 positionN :: Bytes
 positionN = \<open>Markup.positionN\<close>
 position :: T
 position = markup_elem positionN
 
+position_properties :: [Bytes]
+position_properties = [lineN, offsetN, end_offsetN, fileN, idN]
+
+
+{- position "def" names -}
+
+make_def :: Bytes -> Bytes
+make_def a = "def_" <> a
+
+def_names :: Map Bytes Bytes
+def_names = Map.fromList $ map (\a -> (a, make_def a)) position_properties
+
+def_name :: Bytes -> Bytes
+def_name a =
+  case Map.lookup a def_names of
+    Just b -> b
+    Nothing -> make_def a
+
 
 {- expression -}
 
 expressionN :: Bytes
 expressionN = \<open>Markup.expressionN\<close>
 
 expression :: Bytes -> T
 expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
 
 
 {- citation -}
 
 citationN :: Bytes
 citationN = \<open>Markup.citationN\<close>
 citation :: Bytes -> T
 citation = markup_string nameN citationN
 
 
 {- external resources -}
 
 pathN :: Bytes
 pathN = \<open>Markup.pathN\<close>
 path :: Bytes -> T
 path = markup_string pathN nameN
 
 urlN :: Bytes
 urlN = \<open>Markup.urlN\<close>
 url :: Bytes -> T
 url = markup_string urlN nameN
 
 docN :: Bytes
 docN = \<open>Markup.docN\<close>
 doc :: Bytes -> T
 doc = markup_string docN nameN
 
 
 {- pretty printing -}
 
 markupN, consistentN, unbreakableN, indentN :: Bytes
 markupN = \<open>Markup.markupN\<close>
 consistentN = \<open>Markup.consistentN\<close>
 unbreakableN = \<open>Markup.unbreakableN\<close>
 indentN = \<open>Markup.indentN\<close>
 
 widthN :: Bytes
 widthN = \<open>Markup.widthN\<close>
 
 blockN :: Bytes
 blockN = \<open>Markup.blockN\<close>
 block :: Bool -> Int -> T
 block c i =
   (blockN,
     (if c then [(consistentN, Value.print_bool c)] else []) <>
     (if i /= 0 then [(indentN, Value.print_int i)] else []))
 
 breakN :: Bytes
 breakN = \<open>Markup.breakN\<close>
 break :: Int -> Int -> T
 break w i =
   (breakN,
     (if w /= 0 then [(widthN, Value.print_int w)] else []) <>
     (if i /= 0 then [(indentN, Value.print_int i)] else []))
 
 fbreakN :: Bytes
 fbreakN = \<open>Markup.fbreakN\<close>
 fbreak :: T
 fbreak = markup_elem fbreakN
 
 itemN :: Bytes
 itemN = \<open>Markup.itemN\<close>
 item :: T
 item = markup_elem itemN
 
 
 {- text properties -}
 
 wordsN :: Bytes
 wordsN = \<open>Markup.wordsN\<close>
 words :: T
 words = markup_elem wordsN
 
 
 {- inner syntax -}
 
 tfreeN :: Bytes
 tfreeN = \<open>Markup.tfreeN\<close>
 tfree :: T
 tfree = markup_elem tfreeN
 
 tvarN :: Bytes
 tvarN = \<open>Markup.tvarN\<close>
 tvar :: T
 tvar = markup_elem tvarN
 
 freeN :: Bytes
 freeN = \<open>Markup.freeN\<close>
 free :: T
 free = markup_elem freeN
 
 skolemN :: Bytes
 skolemN = \<open>Markup.skolemN\<close>
 skolem :: T
 skolem = markup_elem skolemN
 
 boundN :: Bytes
 boundN = \<open>Markup.boundN\<close>
 bound :: T
 bound = markup_elem boundN
 
 varN :: Bytes
 varN = \<open>Markup.varN\<close>
 var :: T
 var = markup_elem varN
 
 numeralN :: Bytes
 numeralN = \<open>Markup.numeralN\<close>
 numeral :: T
 numeral = markup_elem numeralN
 
 literalN :: Bytes
 literalN = \<open>Markup.literalN\<close>
 literal :: T
 literal = markup_elem literalN
 
 delimiterN :: Bytes
 delimiterN = \<open>Markup.delimiterN\<close>
 delimiter :: T
 delimiter = markup_elem delimiterN
 
 inner_stringN :: Bytes
 inner_stringN = \<open>Markup.inner_stringN\<close>
 inner_string :: T
 inner_string = markup_elem inner_stringN
 
 inner_cartoucheN :: Bytes
 inner_cartoucheN = \<open>Markup.inner_cartoucheN\<close>
 inner_cartouche :: T
 inner_cartouche = markup_elem inner_cartoucheN
 
 
 token_rangeN :: Bytes
 token_rangeN = \<open>Markup.token_rangeN\<close>
 token_range :: T
 token_range = markup_elem token_rangeN
 
 
 sortingN :: Bytes
 sortingN = \<open>Markup.sortingN\<close>
 sorting :: T
 sorting = markup_elem sortingN
 
 typingN :: Bytes
 typingN = \<open>Markup.typingN\<close>
 typing :: T
 typing = markup_elem typingN
 
 class_parameterN :: Bytes
 class_parameterN = \<open>Markup.class_parameterN\<close>
 class_parameter :: T
 class_parameter = markup_elem class_parameterN
 
 
 {- antiquotations -}
 
 antiquotedN :: Bytes
 antiquotedN = \<open>Markup.antiquotedN\<close>
 antiquoted :: T
 antiquoted = markup_elem antiquotedN
 
 antiquoteN :: Bytes
 antiquoteN = \<open>Markup.antiquoteN\<close>
 antiquote :: T
 antiquote = markup_elem antiquoteN
 
 
 {- text structure -}
 
 paragraphN :: Bytes
 paragraphN = \<open>Markup.paragraphN\<close>
 paragraph :: T
 paragraph = markup_elem paragraphN
 
 text_foldN :: Bytes
 text_foldN = \<open>Markup.text_foldN\<close>
 text_fold :: T
 text_fold = markup_elem text_foldN
 
 
 {- outer syntax -}
 
 keyword1N :: Bytes
 keyword1N = \<open>Markup.keyword1N\<close>
 keyword1 :: T
 keyword1 = markup_elem keyword1N
 
 keyword2N :: Bytes
 keyword2N = \<open>Markup.keyword2N\<close>
 keyword2 :: T
 keyword2 = markup_elem keyword2N
 
 keyword3N :: Bytes
 keyword3N = \<open>Markup.keyword3N\<close>
 keyword3 :: T
 keyword3 = markup_elem keyword3N
 
 quasi_keywordN :: Bytes
 quasi_keywordN = \<open>Markup.quasi_keywordN\<close>
 quasi_keyword :: T
 quasi_keyword = markup_elem quasi_keywordN
 
 improperN :: Bytes
 improperN = \<open>Markup.improperN\<close>
 improper :: T
 improper = markup_elem improperN
 
 operatorN :: Bytes
 operatorN = \<open>Markup.operatorN\<close>
 operator :: T
 operator = markup_elem operatorN
 
 stringN :: Bytes
 stringN = \<open>Markup.stringN\<close>
 string :: T
 string = markup_elem stringN
 
 alt_stringN :: Bytes
 alt_stringN = \<open>Markup.alt_stringN\<close>
 alt_string :: T
 alt_string = markup_elem alt_stringN
 
 verbatimN :: Bytes
 verbatimN = \<open>Markup.verbatimN\<close>
 verbatim :: T
 verbatim = markup_elem verbatimN
 
 cartoucheN :: Bytes
 cartoucheN = \<open>Markup.cartoucheN\<close>
 cartouche :: T
 cartouche = markup_elem cartoucheN
 
 commentN :: Bytes
 commentN = \<open>Markup.commentN\<close>
 comment :: T
 comment = markup_elem commentN
 
 
 {- comments -}
 
 comment1N :: Bytes
 comment1N = \<open>Markup.comment1N\<close>
 comment1 :: T
 comment1 = markup_elem comment1N
 
 comment2N :: Bytes
 comment2N = \<open>Markup.comment2N\<close>
 comment2 :: T
 comment2 = markup_elem comment2N
 
 comment3N :: Bytes
 comment3N = \<open>Markup.comment3N\<close>
 comment3 :: T
 comment3 = markup_elem comment3N
 
 
 {- command status -}
 
 forkedN, joinedN, runningN, finishedN, failedN, canceledN,
   initializedN, finalizedN, consolidatedN :: Bytes
 forkedN = \<open>Markup.forkedN\<close>
 joinedN = \<open>Markup.joinedN\<close>
 runningN = \<open>Markup.runningN\<close>
 finishedN = \<open>Markup.finishedN\<close>
 failedN = \<open>Markup.failedN\<close>
 canceledN = \<open>Markup.canceledN\<close>
 initializedN = \<open>Markup.initializedN\<close>
 finalizedN = \<open>Markup.finalizedN\<close>
 consolidatedN = \<open>Markup.consolidatedN\<close>
 
 forked, joined, running, finished, failed, canceled,
   initialized, finalized, consolidated :: T
 forked = markup_elem forkedN
 joined = markup_elem joinedN
 running = markup_elem runningN
 finished = markup_elem finishedN
 failed = markup_elem failedN
 canceled = markup_elem canceledN
 initialized = markup_elem initializedN
 finalized = markup_elem finalizedN
 consolidated = markup_elem consolidatedN
 
 
 {- messages -}
 
 writelnN :: Bytes
 writelnN = \<open>Markup.writelnN\<close>
 writeln :: T
 writeln = markup_elem writelnN
 
 stateN :: Bytes
 stateN = \<open>Markup.stateN\<close>
 state :: T
 state = markup_elem stateN
 
 informationN :: Bytes
 informationN = \<open>Markup.informationN\<close>
 information :: T
 information = markup_elem informationN
 
 tracingN :: Bytes
 tracingN = \<open>Markup.tracingN\<close>
 tracing :: T
 tracing = markup_elem tracingN
 
 warningN :: Bytes
 warningN = \<open>Markup.warningN\<close>
 warning :: T
 warning = markup_elem warningN
 
 legacyN :: Bytes
 legacyN = \<open>Markup.legacyN\<close>
 legacy :: T
 legacy = markup_elem legacyN
 
 errorN :: Bytes
 errorN = \<open>Markup.errorN\<close>
 error :: T
 error = markup_elem errorN
 
 reportN :: Bytes
 reportN = \<open>Markup.reportN\<close>
 report :: T
 report = markup_elem reportN
 
 no_reportN :: Bytes
 no_reportN = \<open>Markup.no_reportN\<close>
 no_report :: T
 no_report = markup_elem no_reportN
 
 intensifyN :: Bytes
 intensifyN = \<open>Markup.intensifyN\<close>
 intensify :: T
 intensify = markup_elem intensifyN
 
 
 {- output -}
 
 type Output = (Bytes, Bytes)
 
 no_output :: Output
 no_output = ("", "")
 \<close>
 
 generate_file "Isabelle/Position.hs" = \<open>
 {-  Title:      Isabelle/Position.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
 symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
 right-open interval offset .. end_offset (exclusive).
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/position.ML\<close>.
 -}
 
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Position (
   T, line_of, column_of, offset_of, end_offset_of, file_of, id_of,
   start, none, put_file, file, file_only, put_id,
   symbol, symbol_explode, symbol_explode_string, shift_offsets,
   of_properties, properties_of, def_properties_of, entity_markup, entity_properties_of,
   is_reported, is_reported_range, here,
 
   Range, no_range, no_range_position, range_position, range
 ) where
 
 import Data.Maybe (isJust, fromMaybe)
+import Data.Bifunctor (first)
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Bytes as Bytes
 import qualified Isabelle.Value as Value
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Markup as Markup
 import qualified Isabelle.YXML as YXML
 import Isabelle.Library
 import qualified Isabelle.Symbol as Symbol
 import Isabelle.Symbol (Symbol)
 
 
 {- position -}
 
 data T =
   Position {
     _line :: Int,
     _column :: Int,
     _offset :: Int,
     _end_offset :: Int,
     _file :: Bytes,
     _id :: Bytes }
   deriving (Eq, Ord)
 
 valid, invalid :: Int -> Bool
 valid i = i > 0
 invalid = not . valid
 
 maybe_valid :: Int -> Maybe Int
 maybe_valid i = if valid i then Just i else Nothing
 
 if_valid :: Int -> Int -> Int
 if_valid i i' = if valid i then i' else i
 
 
 {- fields -}
 
 line_of, column_of, offset_of, end_offset_of :: T -> Maybe Int
 line_of = maybe_valid . _line
 column_of = maybe_valid . _column
 offset_of = maybe_valid . _offset
 end_offset_of = maybe_valid . _end_offset
 
 file_of :: T -> Maybe Bytes
 file_of = proper_string . _file
 
 id_of :: T -> Maybe Bytes
 id_of = proper_string . _id
 
 
 {- make position -}
 
 start :: T
 start = Position 1 1 1 0 Bytes.empty Bytes.empty
 
 none :: T
 none = Position 0 0 0 0 Bytes.empty Bytes.empty
 
 put_file :: Bytes -> T -> T
 put_file file pos = pos { _file = file }
 
 file :: Bytes -> T
 file file = put_file file start
 
 file_only :: Bytes -> T
 file_only file = put_file file none
 
 put_id :: Bytes -> T -> T
 put_id id pos = pos { _id = id }
 
 
 {- count position -}
 
 count_line :: Symbol -> Int -> Int
 count_line "\n" line = if_valid line (line + 1)
 count_line _ line = line
 
 count_column :: Symbol -> Int -> Int
 count_column "\n" column = if_valid column 1
 count_column s column = if Symbol.not_eof s then if_valid column (column + 1) else column
 
 count_offset :: Symbol -> Int -> Int
 count_offset s offset = if Symbol.not_eof s then if_valid offset (offset + 1) else offset
 
 symbol :: Symbol -> T -> T
 symbol s pos =
   pos {
     _line = count_line s (_line pos),
     _column = count_column s (_column pos),
     _offset = count_offset s (_offset pos) }
 
 symbol_explode :: BYTES a => a -> T -> T
 symbol_explode = fold symbol . Symbol.explode . make_bytes
 
 symbol_explode_string :: String -> T -> T
 symbol_explode_string = symbol_explode
 
 
 {- shift offsets -}
 
 shift_offsets :: Int -> T -> T
 shift_offsets shift pos = pos { _offset = offset', _end_offset = end_offset' }
   where
     offset = _offset pos
     end_offset = _end_offset pos
     offset' = if invalid offset || invalid shift then offset else offset + shift
     end_offset' = if invalid end_offset || invalid shift then end_offset else end_offset + shift
 
 
 {- markup properties -}
 
 get_string :: Properties.T -> Bytes -> Bytes
 get_string props name = fromMaybe "" (Properties.get_value Just props name)
 
 get_int :: Properties.T -> Bytes -> Int
 get_int props name = fromMaybe 0 (Properties.get_value Value.parse_int props name)
 
 of_properties :: Properties.T -> T
 of_properties props =
   none {
     _line = get_int props Markup.lineN,
     _offset = get_int props Markup.offsetN,
     _end_offset = get_int props Markup.end_offsetN,
     _file = get_string props Markup.fileN,
     _id = get_string props Markup.idN }
 
 string_entry :: Bytes -> Bytes -> Properties.T
 string_entry k s = if Bytes.null s then [] else [(k, s)]
 
 int_entry :: Bytes -> Int -> Properties.T
 int_entry k i = if invalid i then [] else [(k, Value.print_int i)]
 
 properties_of :: T -> Properties.T
 properties_of pos =
   int_entry Markup.lineN (_line pos) ++
   int_entry Markup.offsetN (_offset pos) ++
   int_entry Markup.end_offsetN (_end_offset pos) ++
   string_entry Markup.fileN (_file pos) ++
   string_entry Markup.idN (_id pos)
 
 def_properties_of :: T -> Properties.T
-def_properties_of = properties_of #> map (\(a, b) -> ("def_" <> a, b))
+def_properties_of = properties_of #> map (first Markup.def_name)
 
 entity_markup :: Bytes -> (Bytes, T) -> Markup.T
 entity_markup kind (name, pos) =
   Markup.entity kind name |> Markup.properties (def_properties_of pos)
 
 entity_properties_of :: Bool -> Int -> T -> Properties.T
 entity_properties_of def serial pos =
   if def then (Markup.defN, Value.print_int serial) : properties_of pos
   else (Markup.refN, Value.print_int serial) : def_properties_of pos
 
 
 {- reports -}
 
 is_reported :: T -> Bool
 is_reported pos = isJust (offset_of pos) && isJust (id_of pos)
 
 is_reported_range :: T -> Bool
 is_reported_range pos = is_reported pos && isJust (end_offset_of pos)
 
 
 {- here: user output -}
 
 here :: T -> Bytes
 here pos = if Bytes.null s2 then "" else s1 <> m1 <> s2 <> m2
   where
     props = properties_of pos
     (m1, m2) = YXML.output_markup (Markup.properties props Markup.position)
     (s1, s2) =
       case (line_of pos, file_of pos) of
         (Just i, Nothing) -> (" ", "(line " <> Value.print_int i <> ")")
         (Just i, Just name) -> (" ", "(line " <> Value.print_int i <> " of " <> quote name <> ")")
         (Nothing, Just name) -> (" ", "(file " <> quote name <> ")")
         _ -> if is_reported pos then ("", "\092<^here>") else ("", "")
 
 
 {- range -}
 
 type Range = (T, T)
 
 no_range :: Range
 no_range = (none, none)
 
 no_range_position :: T -> T
 no_range_position pos = pos { _end_offset = 0 }
 
 range_position :: Range -> T
 range_position (pos, pos') = pos { _end_offset = _offset pos' }
 
 range :: Range -> Range
 range (pos, pos') = (range_position (pos, pos'), no_range_position pos')
 \<close>
 
 generate_file "Isabelle/XML.hs" = \<open>
 {-  Title:      Isabelle/XML.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Untyped XML trees and representation of ML values.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 
 module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
 where
 
 import Isabelle.Library
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Markup as Markup
 import qualified Isabelle.Buffer as Buffer
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 
 
 {- types -}
 
 type Attributes = Properties.T
 type Body = [Tree]
 data Tree = Elem (Markup.T, Body) | Text Bytes
 
 
 {- wrapped elements -}
 
 wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree
 wrap_elem (((a, atts), body1), body2) =
   Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)
 
 unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree])
 unwrap_elem
   (Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)) =
   Just (((a, atts), body1), body2)
 unwrap_elem _ = Nothing
 
 
 {- text content -}
 
 add_content :: Tree -> Buffer.T -> Buffer.T
 add_content tree =
   case unwrap_elem tree of
     Just (_, ts) -> fold add_content ts
     Nothing ->
       case tree of
         Elem (_, ts) -> fold add_content ts
         Text s -> Buffer.add s
 
 content_of :: Body -> Bytes
 content_of body = Buffer.empty |> fold add_content body |> Buffer.content
 
 
 {- string representation -}
 
 encode_char :: Char -> String
 encode_char '<' = "&lt;"
 encode_char '>' = "&gt;"
 encode_char '&' = "&amp;"
 encode_char '\'' = "&apos;"
 encode_char '\"' = "&quot;"
 encode_char c = [c]
 
 encode_text :: Bytes -> Bytes
 encode_text = make_bytes . concatMap (encode_char . Bytes.char) . Bytes.unpack
 
 instance Show Tree where
   show tree =
     Buffer.empty |> show_tree tree |> Buffer.content |> make_string
     where
       show_tree (Elem ((name, atts), [])) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
       show_tree (Elem ((name, atts), ts)) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
         fold show_tree ts #>
         Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
       show_tree (Text s) = Buffer.add (encode_text s)
 
       show_elem name atts =
         space_implode " " (name : map (\(a, x) -> a <> "=\"" <> encode_text x <> "\"") atts)
 \<close>
 
 generate_file "Isabelle/XML/Encode.hs" = \<open>
 {-  Title:      Isabelle/XML/Encode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 XML as data representation language.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 
 module Isabelle.XML.Encode (
   A, T, V, P,
 
   int_atom, bool_atom, unit_atom,
 
   tree, properties, string, int, bool, unit, pair, triple, list, option, variant
 )
 where
 
 import Data.Maybe (fromJust)
 
 import Isabelle.Library
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Value as Value
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.XML as XML
 
 
 type A a = a -> Bytes
 type T a = a -> XML.Body
 type V a = a -> Maybe ([Bytes], XML.Body)
 type P a = a -> [Bytes]
 
 
 -- atomic values
 
 int_atom :: A Int
 int_atom = Value.print_int
 
 bool_atom :: A Bool
 bool_atom False = "0"
 bool_atom True = "1"
 
 unit_atom :: A ()
 unit_atom () = ""
 
 
 -- structural nodes
 
 node ts = XML.Elem ((":", []), ts)
 
 vector = map_index (\(i, x) -> (int_atom i, x))
 
 tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
 
 
 -- representation of standard types
 
 tree :: T XML.Tree
 tree t = [t]
 
 properties :: T Properties.T
 properties props = [XML.Elem ((":", props), [])]
 
 string :: T Bytes
 string "" = []
 string s = [XML.Text s]
 
 int :: T Int
 int = string . int_atom
 
 bool :: T Bool
 bool = string . bool_atom
 
 unit :: T ()
 unit = string . unit_atom
 
 pair :: T a -> T b -> T (a, b)
 pair f g (x, y) = [node (f x), node (g y)]
 
 triple :: T a -> T b -> T c -> T (a, b, c)
 triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
 
 list :: T a -> T [a]
 list f xs = map (node . f) xs
 
 option :: T a -> T (Maybe a)
 option _ Nothing = []
 option f (Just x) = [node (f x)]
 
 variant :: [V a] -> T a
 variant fs x = [tagged (fromJust (get_index (\f -> f x) fs))]
 \<close>
 
 generate_file "Isabelle/XML/Decode.hs" = \<open>
 {-  Title:      Isabelle/XML/Decode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 XML as data representation language.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 
 module Isabelle.XML.Decode (
   A, T, V, P,
 
   int_atom, bool_atom, unit_atom,
 
   tree, properties, string, int, bool, unit, pair, triple, list, option, variant
 )
 where
 
 import Isabelle.Library
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Value as Value
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.XML as XML
 
 
 type A a = Bytes -> a
 type T a = XML.Body -> a
 type V a = ([Bytes], XML.Body) -> a
 type P a = [Bytes] -> a
 
 err_atom = error "Malformed XML atom"
 err_body = error "Malformed XML body"
 
 
 {- atomic values -}
 
 int_atom :: A Int
 int_atom s =
   case Value.parse_int s of
     Just i -> i
     Nothing -> err_atom
 
 bool_atom :: A Bool
 bool_atom "0" = False
 bool_atom "1" = True
 bool_atom _ = err_atom
 
 unit_atom :: A ()
 unit_atom "" = ()
 unit_atom _ = err_atom
 
 
 {- structural nodes -}
 
 node (XML.Elem ((":", []), ts)) = ts
 node _ = err_body
 
 vector atts =
   map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
 
 tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
 tagged _ = err_body
 
 
 {- representation of standard types -}
 
 tree :: T XML.Tree
 tree [t] = t
 tree _ = err_body
 
 properties :: T Properties.T
 properties [XML.Elem ((":", props), [])] = props
 properties _ = err_body
 
 string :: T Bytes
 string [] = ""
 string [XML.Text s] = s
 string _ = err_body
 
 int :: T Int
 int = int_atom . string
 
 bool :: T Bool
 bool = bool_atom . string
 
 unit :: T ()
 unit = unit_atom . string
 
 pair :: T a -> T b -> T (a, b)
 pair f g [t1, t2] = (f (node t1), g (node t2))
 pair _ _ _ = err_body
 
 triple :: T a -> T b -> T c -> T (a, b, c)
 triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
 triple _ _ _ _ = err_body
 
 list :: T a -> T [a]
 list f ts = map (f . node) ts
 
 option :: T a -> T (Maybe a)
 option _ [] = Nothing
 option f [t] = Just (f (node t))
 option _ _ = err_body
 
 variant :: [V a] -> T a
 variant fs [t] = (fs !! tag) (xs, ts)
   where (tag, (xs, ts)) = tagged t
 variant _ _ = err_body
 \<close>
 
 generate_file "Isabelle/YXML.hs" = \<open>
 {-  Title:      Isabelle/YXML.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Efficient text representation of XML trees.  Suitable for direct
 inlining into plain text.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-incomplete-patterns #-}
 
 module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
   buffer_body, buffer, string_of_body, string_of, parse_body, parse)
 where
 
 import qualified Data.List as List
 import Data.Word (Word8)
 
 import Isabelle.Library
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Markup as Markup
 import qualified Isabelle.XML as XML
 import qualified Isabelle.Buffer as Buffer
 
 
 {- markers -}
 
 charX, charY :: Word8
 charX = 5
 charY = 6
 
 strX, strY, strXY, strXYX :: Bytes
 strX = Bytes.singleton charX
 strY = Bytes.singleton charY
 strXY = strX <> strY
 strXYX = strXY <> strX
 
 detect :: Bytes -> Bool
 detect = Bytes.any (\c -> c == charX || c == charY)
 
 
 {- output -}
 
 output_markup :: Markup.T -> Markup.Output
 output_markup markup@(name, atts) =
   if Markup.is_empty markup then Markup.no_output
   else (strXY <> name <> Bytes.concat (map (\(a, x) -> strY <> a <> "=" <> x) atts) <> strX, strXYX)
 
 buffer_attrib (a, x) =
   Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
 
 buffer_body :: XML.Body -> Buffer.T -> Buffer.T
 buffer_body = fold buffer
 
 buffer :: XML.Tree -> Buffer.T -> Buffer.T
 buffer (XML.Elem ((name, atts), ts)) =
   Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
   buffer_body ts #>
   Buffer.add strXYX
 buffer (XML.Text s) = Buffer.add s
 
 string_of_body :: XML.Body -> Bytes
 string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
 
 string_of :: XML.Tree -> Bytes
 string_of = string_of_body . single
 
 
 {- parse -}
 
 -- split: fields or non-empty tokens
 
 split :: Bool -> Word8 -> [Word8] -> [[Word8]]
 split _ _ [] = []
 split fields sep str = splitting str
   where
     splitting rest =
       case span (/= sep) rest of
         (_, []) -> cons rest []
         (prfx, _ : rest') -> cons prfx (splitting rest')
     cons item = if fields || not (null item) then (:) item else id
 
 
 -- structural errors
 
 err :: Bytes -> a
 err msg = error (make_string ("Malformed YXML: " <> msg))
 
 err_attribute = err "bad attribute"
 err_element = err "bad element"
 
 err_unbalanced :: Bytes -> a
 err_unbalanced name =
   if Bytes.null name then err "unbalanced element"
   else err ("unbalanced element " <> quote name)
 
 
 -- stack operations
 
 add x ((elem, body) : pending) = (elem, x : body) : pending
 
 push name atts pending =
   if Bytes.null name then err_element
   else ((name, atts), []) : pending
 
 pop (((name, atts), body) : pending) =
   if Bytes.null name then err_unbalanced name
   else add (XML.Elem ((name, atts), reverse body)) pending
 
 
 -- parsing
 
 parse_attrib s =
   case List.elemIndex (Bytes.byte '=') s of
     Just i | i > 0 -> (Bytes.pack $ take i s, Bytes.pack $ drop (i + 1) s)
     _ -> err_attribute
 
 parse_chunk [[], []] = pop
 parse_chunk ([] : name : atts) = push (Bytes.pack name) (map parse_attrib atts)
 parse_chunk txts = fold (add . XML.Text . Bytes.pack) txts
 
 parse_body :: Bytes -> XML.Body
 parse_body source =
   case fold parse_chunk chunks [((Bytes.empty, []), [])] of
     [((name, _), result)] | Bytes.null name -> reverse result
     ((name, _), _) : _ -> err_unbalanced name
   where chunks = source |> Bytes.unpack |> split False charX |> map (split True charY)
 
 parse :: Bytes -> XML.Tree
 parse source =
   case parse_body source of
     [result] -> result
     [] -> XML.Text ""
     _ -> err "multiple results"
 \<close>
 
 generate_file "Isabelle/Completion.hs" = \<open>
 {-  Title:      Isabelle/Completion.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Completion of names.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Completion (
     Name, T, names, none, make, markup_element, markup_report, make_report
   ) where
 
 import qualified Isabelle.Bytes as Bytes
 import qualified Isabelle.Name as Name
 import Isabelle.Name (Name)
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Markup as Markup
 import Isabelle.XML.Classes
 import qualified Isabelle.XML as XML
 import qualified Isabelle.YXML as YXML
 
 
 type Names = [(Name, (Name, Name))]  -- external name, kind, internal name
 data T = Completion Properties.T Int Names  -- position, total length, names
 
 names :: Int -> Properties.T -> Names -> T
 names limit props names = Completion props (length names) (take limit names)
 
 none :: T
 none = names 0 [] []
 
 make :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> T
 make limit (name, props) make_names =
   if name /= "" && name /= "_" then
     names limit props (make_names (Bytes.isPrefixOf (Name.clean name)))
   else none
 
 markup_element :: T -> (Markup.T, XML.Body)
 markup_element (Completion props total names) =
   if not (null names) then
     (Markup.properties props Markup.completion, encode (total, names))
   else (Markup.empty, [])
 
 markup_report :: [T] -> Name
 markup_report [] = Bytes.empty
 markup_report elems =
   YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
 
 make_report :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> Name
 make_report limit name_props make_names =
   markup_report [make limit name_props make_names]
 \<close>
 
 generate_file "Isabelle/File.hs" = \<open>
 {-  Title:      Isabelle/File.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 File-system operations.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
 -}
 
 module Isabelle.File (read, write, append) where
 
 import Prelude hiding (read)
 import qualified System.IO as IO
 import qualified Data.ByteString as ByteString
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 
 read :: IO.FilePath -> IO Bytes
 read path = Bytes.make <$> IO.withFile path IO.ReadMode ByteString.hGetContents
 
 write :: IO.FilePath -> Bytes -> IO ()
 write path bs = IO.withFile path IO.WriteMode (\h -> ByteString.hPut h (Bytes.unmake bs))
 
 append :: IO.FilePath -> Bytes -> IO ()
 append path bs = IO.withFile path IO.AppendMode (\h -> ByteString.hPut h (Bytes.unmake bs))
 \<close>
 
 generate_file "Isabelle/Pretty.hs" = \<open>
 {-  Title:      Isabelle/Pretty.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Generic pretty printing module.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 
 module Isabelle.Pretty (
   T, symbolic, formatted, unformatted,
 
   str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
   item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
   commas, enclose, enum, list, str_list, big_list)
 where
 
 import qualified Data.List as List
 
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import Isabelle.Library hiding (quote, separate, commas)
 import qualified Isabelle.Buffer as Buffer
 import qualified Isabelle.Markup as Markup
 import qualified Isabelle.XML as XML
 import qualified Isabelle.YXML as YXML
 
 
 data T =
     Block Markup.T Bool Int [T]
   | Break Int Int
   | Str Bytes
 
 
 {- output -}
 
 symbolic_text s = if Bytes.null s then [] else [XML.Text s]
 
 symbolic_markup markup body =
   if Markup.is_empty markup then body
   else [XML.Elem (markup, body)]
 
 symbolic :: T -> XML.Body
 symbolic (Block markup consistent indent prts) =
   concatMap symbolic prts
   |> symbolic_markup block_markup
   |> symbolic_markup markup
   where block_markup = if null prts then Markup.empty else Markup.block consistent indent
 symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (Bytes.spaces wd))]
 symbolic (Str s) = symbolic_text s
 
 formatted :: T -> Bytes
 formatted = YXML.string_of_body . symbolic
 
 unformatted :: T -> Bytes
 unformatted prt = Buffer.empty |> out prt |> Buffer.content
   where
     out (Block markup _ _ prts) =
       let (bg, en) = YXML.output_markup markup
       in Buffer.add bg #> fold out prts #> Buffer.add en
     out (Break _ wd) = Buffer.add (Bytes.spaces wd)
     out (Str s) = Buffer.add s
 
 
 {- derived operations to create formatting expressions -}
 
 force_nat n | n < 0 = 0
 force_nat n = n
 
 str :: BYTES a => a -> T
 str = Str . make_bytes
 
 brk_indent :: Int -> Int -> T
 brk_indent wd ind = Break (force_nat wd) ind
 
 brk :: Int -> T
 brk wd = brk_indent wd 0
 
 fbrk :: T
 fbrk = Str "\n"
 
 breaks, fbreaks :: [T] -> [T]
 breaks = List.intersperse (brk 1)
 fbreaks = List.intersperse fbrk
 
 blk :: (Int, [T]) -> T
 blk (indent, es) = Block Markup.empty False (force_nat indent) es
 
 block :: [T] -> T
 block prts = blk (2, prts)
 
 strs :: BYTES a => [a] -> T
 strs = block . breaks . map str
 
 markup :: Markup.T -> [T] -> T
 markup m = Block m False 0
 
 mark :: Markup.T -> T -> T
 mark m prt = if m == Markup.empty then prt else markup m [prt]
 
 mark_str :: BYTES a => (Markup.T, a) -> T
 mark_str (m, s) = mark m (str s)
 
 marks_str :: BYTES a => ([Markup.T], a) -> T
 marks_str (ms, s) = fold_rev mark ms (str s)
 
 item :: [T] -> T
 item = markup Markup.item
 
 text_fold :: [T] -> T
 text_fold = markup Markup.text_fold
 
 keyword1, keyword2 :: BYTES a => a -> T
 keyword1 name = mark_str (Markup.keyword1, name)
 keyword2 name = mark_str (Markup.keyword2, name)
 
 text :: BYTES a => a -> [T]
 text = breaks . map str . filter (not . Bytes.null) . space_explode ' ' . make_bytes
 
 paragraph :: [T] -> T
 paragraph = markup Markup.paragraph
 
 para :: BYTES a => a -> T
 para = paragraph . text
 
 quote :: T -> T
 quote prt = blk (1, [Str "\"", prt, Str "\""])
 
 cartouche :: T -> T
 cartouche prt = blk (1, [Str "\92<open>", prt, Str "\92<close>"])
 
 separate :: BYTES a => a -> [T] -> [T]
 separate sep = List.intercalate [str sep, brk 1] . map single
 
 commas :: [T] -> [T]
 commas = separate ("," :: Bytes)
 
 enclose :: BYTES a => a -> a -> [T] -> T
 enclose lpar rpar prts = block (str lpar : prts <> [str rpar])
 
 enum :: BYTES a => a -> a -> a -> [T] -> T
 enum sep lpar rpar = enclose lpar rpar . separate sep
 
 list :: BYTES a => a -> a -> [T] -> T
 list = enum ","
 
 str_list :: BYTES a => a -> a -> [a] -> T
 str_list lpar rpar = list lpar rpar . map str
 
 big_list :: BYTES a => a -> [T] -> T
 big_list name prts = block (fbreaks (str name : prts))
 \<close>
 
 generate_file "Isabelle/Name.hs" = \<open>
 {-  Title:      Isabelle/Name.hs
     Author:     Makarius
 
 Names of basic logical entities (variables etc.).
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/name.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Name (
   Name, clean_index, clean,
   Context, declare, is_declared, context, make_context, variant
 )
 where
 
 import Data.Word (Word8)
 import qualified Data.Set as Set
 import Data.Set (Set)
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Symbol as Symbol
 import Isabelle.Library
 
 
 type Name = Bytes
 
 
 {- suffix for internal names -}
 
 underscore :: Word8
 underscore = Bytes.byte '_'
 
 clean_index :: Name -> (Name, Int)
 clean_index x =
   if Bytes.null x || Bytes.last x /= underscore then (x, 0)
   else
     let
       rev = reverse (Bytes.unpack x)
       n = length (takeWhile (== underscore) rev)
       y = Bytes.pack (reverse (drop n rev))
     in (y, n)
 
 clean :: Name -> Name
 clean = fst . clean_index
 
 
 {- context for used names -}
 
 data Context = Context (Set Name)
 
 declare :: Name -> Context -> Context
 declare x (Context names) = Context (Set.insert x names)
 
 is_declared :: Context -> Name -> Bool
 is_declared (Context names) x = Set.member x names
 
 context :: Context
 context = Context (Set.fromList ["", "'"])
 
 make_context :: [Name] -> Context
 make_context used = fold declare used context
 
 
 {- generating fresh names -}
 
 bump_init :: Name -> Name
 bump_init str = str <> "a"
 
 bump_string :: Name -> Name
 bump_string str =
   let
     a = Bytes.byte 'a'
     z = Bytes.byte 'z'
     bump (b : bs) | b == z = a : bump bs
     bump (b : bs) | a <= b && b < z = b + 1 : bs
     bump bs = a : bs
 
     rev = reverse (Bytes.unpack str)
     part2 = reverse (takeWhile (Symbol.is_ascii_quasi . Bytes.char) rev)
     part1 = reverse (bump (drop (length part2) rev))
   in Bytes.pack (part1 <> part2)
 
 variant :: Name -> Context -> (Name, Context)
 variant name names =
   let
     vary bump x = if is_declared names x then bump x |> vary bump_string else x
     (x, n) = clean_index name
     x' = x |> vary bump_init
     names' = declare x' names;
   in (x' <> Bytes.pack (replicate n underscore), names')
 \<close>
 
 generate_file "Isabelle/Term.hs" = \<open>
 {-  Title:      Isabelle/Term.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Lambda terms, types, sorts.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Term (
   Indexname, Sort, Typ(..), Term(..),
   Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs,
   type_op0, type_op1, op0, op1, op2, typed_op2, binder,
   dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
   aconv, list_comb, strip_comb, head_of
 )
 where
 
 import Isabelle.Library
 import qualified Isabelle.Name as Name
 import Isabelle.Name (Name)
 
 infixr 5 -->
 infixr --->
 
 
 {- types and terms -}
 
 type Indexname = (Name, Int)
 
 type Sort = [Name]
 
 data Typ =
     Type (Name, [Typ])
   | TFree (Name, Sort)
   | TVar (Indexname, Sort)
   deriving (Show, Eq, Ord)
 
 data Term =
     Const (Name, [Typ])
   | Free (Name, Typ)
   | Var (Indexname, Typ)
   | Bound Int
   | Abs (Name, Typ, Term)
   | App (Term, Term)
   deriving (Show, Eq, Ord)
 
 
 {- free and bound variables -}
 
 type Free = (Name, Typ)
 
 lambda :: Free -> Term -> Term
 lambda (name, typ) body = Abs (name, typ, abstract 0 body)
   where
     abstract lev (Free (x, ty)) | name == x && typ == ty = Bound lev
     abstract lev (Abs (a, ty, t)) = Abs (a, ty, abstract (lev + 1) t)
     abstract lev (App (t, u)) = App (abstract lev t, abstract lev u)
     abstract _ t = t
 
 declare_frees :: Term -> Name.Context -> Name.Context
 declare_frees (Free (x, _)) = Name.declare x
 declare_frees (Abs (_, _, b)) = declare_frees b
 declare_frees (App (t, u)) = declare_frees t #> declare_frees u
 declare_frees _ = id
 
 incr_boundvars :: Int -> Term -> Term
 incr_boundvars inc = if inc == 0 then id else incr 0
   where
     incr lev (Bound i) = if i >= lev then Bound (i + inc) else Bound i
     incr lev (Abs (a, ty, b)) = Abs (a, ty, incr (lev + 1) b)
     incr lev (App (t, u)) = App (incr lev t, incr lev u)
     incr _ t = t
 
 subst_bound :: Term -> Term -> Term
 subst_bound arg = subst 0
   where
     subst lev (Bound i) =
       if i < lev then Bound i
       else if i == lev then incr_boundvars lev arg
       else Bound (i - 1)
     subst lev (Abs (a, ty, b)) = Abs (a, ty, subst (lev + 1) b)
     subst lev (App (t, u)) = App (subst lev t, subst lev u)
     subst _ t = t
 
 dest_abs :: Name.Context -> Term -> Maybe (Free, Term)
 dest_abs names (Abs (x, ty, b)) =
   let
     (x', _) = Name.variant x (declare_frees b names)
     v = (x', ty)
   in Just (v, subst_bound (Free v) b)
 dest_abs _ _ = Nothing
 
 strip_abs :: Name.Context -> Term -> ([Free], Term)
 strip_abs names tm =
   case dest_abs names tm of
     Just (v, t) ->
       let (vs, t') = strip_abs names t'
       in (v : vs, t')
     Nothing -> ([], tm)
 
 
 {- type and term operators -}
 
 type_op0 :: Name -> (Typ, Typ -> Bool)
 type_op0 name = (mk, is)
   where
     mk = Type (name, [])
     is (Type (name, _)) = True
     is _ = False
 
 type_op1 :: Name -> (Typ -> Typ, Typ -> Maybe Typ)
 type_op1 name = (mk, dest)
   where
     mk ty = Type (name, [ty])
     dest (Type (name, [ty])) = Just ty
     dest _ = Nothing
 
 type_op2 :: Name -> (Typ -> Typ -> Typ, Typ -> Maybe (Typ, Typ))
 type_op2 name = (mk, dest)
   where
     mk ty1 ty2 = Type (name, [ty1, ty2])
     dest (Type (name, [ty1, ty2])) = Just (ty1, ty2)
     dest _ = Nothing
 
 op0 :: Name -> (Term, Term -> Bool)
 op0 name = (mk, is)
   where
     mk = Const (name, [])
     is (Const (c, _)) = c == name
     is _ = False
 
 op1 :: Name -> (Term -> Term, Term -> Maybe Term)
 op1 name = (mk, dest)
   where
     mk t = App (Const (name, []), t)
     dest (App (Const (c, _), t)) | c == name = Just t
     dest _ = Nothing
 
 op2 :: Name -> (Term -> Term -> Term, Term -> Maybe (Term, Term))
 op2 name = (mk, dest)
   where
     mk t u = App (App (Const (name, []), t), u)
     dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
     dest _ = Nothing
 
 typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term))
 typed_op2 name = (mk, dest)
   where
     mk ty t u = App (App (Const (name, [ty]), t), u)
     dest (App (App (Const (c, [ty]), t), u)) | c == name = Just (ty, t, u)
     dest _ = Nothing
 
 binder :: Name -> (Free -> Term -> Term, Name.Context -> Term -> Maybe (Free, Term))
 binder name = (mk, dest)
   where
     mk (a, ty) b = App (Const (name, [ty]), lambda (a, ty) b)
     dest names (App (Const (c, _), t)) | c == name = dest_abs names t
     dest _ _ = Nothing
 
 
 {- type operations -}
 
 dummyS :: Sort
 dummyS = [""]
 
 dummyT :: Typ; is_dummyT :: Typ -> Bool
 (dummyT, is_dummyT) = type_op0 \<open>\<^type_name>\<open>dummy\<close>\<close>
 
 propT :: Typ; is_propT :: Typ -> Bool
 (propT, is_propT) = type_op0 \<open>\<^type_name>\<open>prop\<close>\<close>
 
 (-->) :: Typ -> Typ -> Typ; dest_funT :: Typ -> Maybe (Typ, Typ)
 ((-->), dest_funT) = type_op2 \<open>\<^type_name>\<open>fun\<close>\<close>
 
 (--->) :: [Typ] -> Typ -> Typ
 [] ---> b = b
 (a : as) ---> b = a --> (as ---> b)
 
 
 {- term operations -}
 
 aconv :: Term -> Term -> Bool
 aconv (App (t1, u1)) (App (t2, u2)) = aconv t1 t2 && aconv u1 u2
 aconv (Abs (_, ty1, t1)) (Abs (_, ty2, t2)) = aconv t1 t2 && ty1 == ty2
 aconv a1 a2 = a1 == a2
 
 list_comb :: Term -> [Term] -> Term
 list_comb f [] = f
 list_comb f (t : ts) = list_comb (App (f, t)) ts
 
 strip_comb :: Term -> (Term, [Term])
 strip_comb tm = strip (tm, [])
   where
     strip (App (f, t), ts) = strip (f, t : ts)
     strip x = x
 
 head_of :: Term -> Term
 head_of (App (f, _)) = head_of f
 head_of u = u
 \<close>
 
 generate_file "Isabelle/Pure.hs" = \<open>
 {-  Title:      Isabelle/Term.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Support for Isabelle/Pure logic.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/logic.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Pure (
   mk_forall, dest_forall, mk_equals, dest_equals, mk_implies, dest_implies
 )
 where
 
 import qualified Isabelle.Name as Name
 import Isabelle.Term
 
 mk_forall :: Free -> Term -> Term; dest_forall :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_forall, dest_forall) = binder \<open>\<^const_name>\<open>Pure.all\<close>\<close>
 
 mk_equals :: Typ -> Term -> Term -> Term; dest_equals :: Term -> Maybe (Typ, Term, Term)
 (mk_equals, dest_equals) = typed_op2 \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
 
 mk_implies :: Term -> Term -> Term; dest_implies :: Term -> Maybe (Term, Term)
 (mk_implies, dest_implies) = op2 \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
 \<close>
 
 generate_file "Isabelle/HOL.hs" = \<open>
 {-  Title:      Isabelle/Term.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Support for Isabelle/HOL logic.
 
 See \<^file>\<open>$ISABELLE_HOME/src/HOL/Tools/hologic.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.HOL (
   boolT, is_boolT, mk_trueprop, dest_trueprop,
   mk_setT, dest_setT, mk_mem, dest_mem,
   mk_eq, dest_eq, true, is_true, false, is_false,
   mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj,
   mk_imp, dest_imp, mk_iff, dest_iff,
   mk_all, dest_all, mk_ex, dest_ex
 )
 where
 
 import qualified Isabelle.Name as Name
 import Isabelle.Term
 
 
 boolT :: Typ; is_boolT :: Typ -> Bool
 (boolT, is_boolT) = type_op0 \<open>\<^type_name>\<open>bool\<close>\<close>
 
 mk_trueprop :: Term -> Term; dest_trueprop :: Term -> Maybe Term
 (mk_trueprop, dest_trueprop) = op1 \<open>\<^const_name>\<open>Trueprop\<close>\<close>
 
 mk_setT :: Typ -> Typ; dest_setT :: Typ -> Maybe Typ
 (mk_setT, dest_setT) = type_op1 \<open>\<^type_name>\<open>set\<close>\<close>
 
 mk_mem :: Typ -> Term -> Term -> Term; dest_mem :: Term -> Maybe (Typ, Term, Term)
 (mk_mem, dest_mem) = typed_op2 \<open>\<^const_name>\<open>Set.member\<close>\<close>
 
 mk_eq :: Typ -> Term -> Term -> Term; dest_eq :: Term -> Maybe (Typ, Term, Term)
 (mk_eq, dest_eq) = typed_op2 \<open>\<^const_name>\<open>HOL.eq\<close>\<close>
 
 true :: Term; is_true :: Term -> Bool
 (true, is_true) = op0 \<open>\<^const_name>\<open>True\<close>\<close>
 
 false :: Term; is_false :: Term -> Bool
 (false, is_false) = op0 \<open>\<^const_name>\<open>False\<close>\<close>
 
 mk_not :: Term -> Term; dest_not :: Term -> Maybe Term
 (mk_not, dest_not) = op1 \<open>\<^const_name>\<open>Not\<close>\<close>
 
 mk_conj :: Term -> Term -> Term; dest_conj :: Term -> Maybe (Term, Term)
 (mk_conj, dest_conj) = op2 \<open>\<^const_name>\<open>conj\<close>\<close>
 
 mk_disj :: Term -> Term -> Term; dest_disj :: Term -> Maybe (Term, Term)
 (mk_disj, dest_disj) = op2 \<open>\<^const_name>\<open>disj\<close>\<close>
 
 mk_imp :: Term -> Term -> Term; dest_imp :: Term -> Maybe (Term, Term)
 (mk_imp, dest_imp) = op2 \<open>\<^const_name>\<open>implies\<close>\<close>
 
 mk_iff :: Term -> Term -> Term
 mk_iff = mk_eq boolT
 
 dest_iff :: Term -> Maybe (Term, Term)
 dest_iff tm =
   case dest_eq tm of
     Just (ty, t, u) | ty == boolT -> Just (t, u)
     _ -> Nothing
 
 mk_all :: Free -> Term -> Term; dest_all :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_all, dest_all) = binder \<open>\<^const_name>\<open>All\<close>\<close>
 
 mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_ex, dest_ex) = binder \<open>\<^const_name>\<open>Ex\<close>\<close>
 \<close>
 
 generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
 {-  Title:      Isabelle/Term_XML/Encode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 XML data representation of lambda terms.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
 -}
 
 {-# LANGUAGE LambdaCase #-}
 
 module Isabelle.Term_XML.Encode (indexname, sort, typ, typ_body, term)
 where
 
 import Isabelle.Library
 import Isabelle.XML.Encode
 import Isabelle.Term
 
 indexname :: P Indexname
 indexname (a, b) = if b == 0 then [a] else [a, int_atom b]
 
 sort :: T Sort
 sort = list string
 
 typ :: T Typ
 typ ty =
   ty |> variant
    [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
     \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
     \case { TVar (a, b) -> Just (indexname a, sort b); _ -> Nothing }]
 
 typ_body :: T Typ
 typ_body ty = if is_dummyT ty then [] else typ ty
 
 term :: T Term
 term t =
   t |> variant
    [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing },
     \case { Free (a, b) -> Just ([a], typ_body b); _ -> Nothing },
     \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing },
     \case { Bound a -> Just ([], int a); _ -> Nothing },
     \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
     \case { App a -> Just ([], pair term term a); _ -> Nothing }]
 \<close>
 
 generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
 {-  Title:      Isabelle/Term_XML/Decode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 XML data representation of lambda terms.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
 -}
 
 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
 
 module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term)
 where
 
 import Isabelle.Library
 import Isabelle.XML.Decode
 import Isabelle.Term
 
 
 indexname :: P Indexname
 indexname [a] = (a, 0)
 indexname [a, b] = (a, int_atom b)
 
 sort :: T Sort
 sort = list string
 
 typ :: T Typ
 typ ty =
   ty |> variant
   [\([a], b) -> Type (a, list typ b),
    \([a], b) -> TFree (a, sort b),
    \(a, b) -> TVar (indexname a, sort b)]
 
 typ_body :: T Typ
 typ_body [] = dummyT
 typ_body body = typ body
 
 term :: T Term
 term t =
   t |> variant
    [\([a], b) -> Const (a, list typ b),
     \([a], b) -> Free (a, typ_body b),
     \(a, b) -> Var (indexname a, typ_body b),
     \([], a) -> Bound (int a),
     \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
     \([], a) -> App (pair term term a)]
 \<close>
 
 generate_file "Isabelle/XML/Classes.hs" = \<open>
 {- generated by Isabelle -}
 
 {-  Title:      Isabelle/XML/Classes.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Type classes for XML data representation.
 -}
 
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 
 module Isabelle.XML.Classes
   (Encode_Atom(..), Decode_Atom(..), Encode (..), Decode (..))
 where
 
 import qualified Isabelle.XML as XML
 import qualified Isabelle.XML.Encode as Encode
 import qualified Isabelle.XML.Decode as Decode
 import qualified Isabelle.Term_XML.Encode as Encode
 import qualified Isabelle.Term_XML.Decode as Decode
 import qualified Isabelle.Properties as Properties
 import Isabelle.Bytes (Bytes)
 import Isabelle.Term (Typ, Term)
 
 
 class Encode_Atom a where encode_atom :: Encode.A a
 class Decode_Atom a where decode_atom :: Decode.A a
 
 instance Encode_Atom Int where encode_atom = Encode.int_atom
 instance Decode_Atom Int where decode_atom = Decode.int_atom
 
 instance Encode_Atom Bool where encode_atom = Encode.bool_atom
 instance Decode_Atom Bool where decode_atom = Decode.bool_atom
 
 instance Encode_Atom () where encode_atom = Encode.unit_atom
 instance Decode_Atom () where decode_atom = Decode.unit_atom
 
 
 class Encode a where encode :: Encode.T a
 class Decode a where decode :: Decode.T a
 
 instance Encode Bytes where encode = Encode.string
 instance Decode Bytes where decode = Decode.string
 
 instance Encode Int where encode = Encode.int
 instance Decode Int where decode = Decode.int
 
 instance Encode Bool where encode = Encode.bool
 instance Decode Bool where decode = Decode.bool
 
 instance Encode () where encode = Encode.unit
 instance Decode () where decode = Decode.unit
 
 instance (Encode a, Encode b) => Encode (a, b)
   where encode = Encode.pair encode encode
 instance (Decode a, Decode b) => Decode (a, b)
   where decode = Decode.pair decode decode
 
 instance (Encode a, Encode b, Encode c) => Encode (a, b, c)
   where encode = Encode.triple encode encode encode
 instance (Decode a, Decode b, Decode c) => Decode (a, b, c)
   where decode = Decode.triple decode decode decode
 
 instance Encode a => Encode [a] where encode = Encode.list encode
 instance Decode a => Decode [a] where decode = Decode.list decode
 
 instance Encode a => Encode (Maybe a) where encode = Encode.option encode
 instance Decode a => Decode (Maybe a) where decode = Decode.option decode
 
 instance Encode XML.Tree where encode = Encode.tree
 instance Decode XML.Tree where decode = Decode.tree
 
 instance Encode Properties.T where encode = Encode.properties
 instance Decode Properties.T where decode = Decode.properties
 
 instance Encode Typ where encode = Encode.typ
 instance Decode Typ where decode = Decode.typ
 
 instance Encode Term where encode = Encode.term
 instance Decode Term where decode = Decode.term
 \<close>
 
 generate_file "Isabelle/UUID.hs" = \<open>
 {-  Title:      Isabelle/UUID.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Universally unique identifiers.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/uuid.scala\<close>.
 -}
 
 module Isabelle.UUID (T, random, print, parse)
 where
 
 import Prelude hiding (print)
 
 import Data.UUID (UUID)
 import qualified Data.UUID as UUID
 import Data.UUID.V4 (nextRandom)
 
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 
 
 type T = UUID
 
 random :: IO T
 random = nextRandom
 
 print :: T -> Bytes
 print = Bytes.make . UUID.toASCIIBytes
 
 parse :: Bytes -> Maybe T
 parse = UUID.fromASCIIBytes . Bytes.unmake
 \<close>
 
 generate_file "Isabelle/Byte_Message.hs" = \<open>
 {-  Title:      Isabelle/Byte_Message.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Byte-oriented messages.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\<close>
 and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
 
 module Isabelle.Byte_Message (
     write, write_line,
     read, read_block, read_line,
     make_message, write_message, read_message,
     make_line_message, write_line_message, read_line_message,
     read_yxml, write_yxml
   )
 where
 
 import Prelude hiding (read)
 import Data.Maybe
 import qualified Data.ByteString as ByteString
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Symbol as Symbol
 import qualified Isabelle.UTF8 as UTF8
 import qualified Isabelle.XML as XML
 import qualified Isabelle.YXML as YXML
 
 import Network.Socket (Socket)
 import qualified Network.Socket.ByteString as Socket
 
 import Isabelle.Library
 import qualified Isabelle.Value as Value
 
 
 {- output operations -}
 
 write :: Socket -> [Bytes] -> IO ()
 write socket = Socket.sendMany socket . map Bytes.unmake
 
 write_line :: Socket -> Bytes -> IO ()
 write_line socket s = write socket [s, "\n"]
 
 
 {- input operations -}
 
 read :: Socket -> Int -> IO Bytes
 read socket n = read_body 0 []
   where
     result = Bytes.concat . reverse
     read_body len ss =
       if len >= n then return (result ss)
       else
         (do
           s <- Socket.recv socket (min (n - len) 8192)
           case ByteString.length s of
             0 -> return (result ss)
             m -> read_body (len + m) (Bytes.make s : ss))
 
 read_block :: Socket -> Int -> IO (Maybe Bytes, Int)
 read_block socket n = do
   msg <- read socket n
   let len = Bytes.length msg
   return (if len == n then Just msg else Nothing, len)
 
 read_line :: Socket -> IO (Maybe Bytes)
 read_line socket = read_body []
   where
     result = trim_line . Bytes.pack . reverse
     read_body bs = do
       s <- Socket.recv socket 1
       case ByteString.length s of
         0 -> return (if null bs then Nothing else Just (result bs))
         1 ->
           case ByteString.head s of
             10 -> return (Just (result bs))
             b -> read_body (b : bs)
 
 
 {- messages with multiple chunks (arbitrary content) -}
 
 make_header :: [Int] -> [Bytes]
 make_header ns = [space_implode "," (map Value.print_int ns), "\n"]
 
 make_message :: [Bytes] -> [Bytes]
 make_message chunks = make_header (map Bytes.length chunks) <> chunks
 
 write_message :: Socket -> [Bytes] -> IO ()
 write_message socket = write socket . make_message
 
 parse_header :: Bytes -> [Int]
 parse_header line =
   let
     res = map Value.parse_nat (space_explode ',' line)
   in
     if all isJust res then map fromJust res
     else error ("Malformed message header: " <> quote (UTF8.decode line))
 
 read_chunk :: Socket -> Int -> IO Bytes
 read_chunk socket n = do
   res <- read_block socket n
   return $
     case res of
       (Just chunk, _) -> chunk
       (Nothing, len) ->
         error ("Malformed message chunk: unexpected EOF after " <>
           show len <> " of " <> show n <> " bytes")
 
 read_message :: Socket -> IO (Maybe [Bytes])
 read_message socket = do
   res <- read_line socket
   case res of
     Just line -> Just <$> mapM (read_chunk socket) (parse_header line)
     Nothing -> return Nothing
 
 
 -- hybrid messages: line or length+block (with content restriction)
 
 is_length :: Bytes -> Bool
 is_length msg =
   not (Bytes.null msg) && Bytes.all_char (\c -> '0' <= c && c <= '9') msg
 
 is_terminated :: Bytes -> Bool
 is_terminated msg =
   not (Bytes.null msg) && Symbol.is_ascii_line_terminator (Bytes.char $ Bytes.last msg)
 
 make_line_message :: Bytes -> [Bytes]
 make_line_message msg =
   let n = Bytes.length msg in
     if is_length msg || is_terminated msg then
       error ("Bad content for line message:\n" <> take 100 (UTF8.decode msg))
     else
       (if n > 100 || Bytes.any_char (== '\n') msg then make_header [n + 1] else []) <> [msg, "\n"]
 
 write_line_message :: Socket -> Bytes -> IO ()
 write_line_message socket = write socket . make_line_message
 
 read_line_message :: Socket -> IO (Maybe Bytes)
 read_line_message socket = do
   opt_line <- read_line socket
   case opt_line of
     Nothing -> return Nothing
     Just line ->
       case Value.parse_nat line of
         Nothing -> return $ Just line
         Just n -> fmap trim_line . fst <$> read_block socket n
 
 
 read_yxml :: Socket -> IO (Maybe XML.Body)
 read_yxml socket = do
   res <- read_line_message socket
   return (YXML.parse_body <$> res)
 
 write_yxml :: Socket -> XML.Body -> IO ()
 write_yxml socket body =
   write_line_message socket (YXML.string_of_body body)
 \<close>
 
 generate_file "Isabelle/Isabelle_Thread.hs" = \<open>
 {-  Title:      Isabelle/Isabelle_Thread.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Isabelle-specific thread management.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.ML\<close>
 and \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.scala\<close>.
 -}
 
 {-# LANGUAGE NamedFieldPuns #-}
 
 module Isabelle.Isabelle_Thread (
   ThreadId, Result,
   find_id,
   properties, change_properties,
   add_resource, del_resource, bracket_resource,
   is_stopped, expose_stopped, stop,
   my_uuid, stop_uuid,
   Fork, fork_finally, fork)
 where
 
 import Data.Unique
 import Data.IORef
 import System.IO.Unsafe
 
 import qualified Data.List as List
 import Control.Monad (when, forM_)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Control.Exception as Exception
 import Control.Concurrent (ThreadId)
 import qualified Control.Concurrent as Concurrent
 import Control.Concurrent.Thread (Result)
 import qualified Control.Concurrent.Thread as Thread
 import qualified Isabelle.UUID as UUID
 import qualified Isabelle.Properties as Properties
 
 
 {- thread info -}
 
 type Resources = Map Unique (IO ())
 data Info = Info {uuid :: UUID.T, props :: Properties.T, stopped :: Bool, resources :: Resources}
 type Infos = Map ThreadId Info
 
 lookup_info :: Infos -> ThreadId -> Maybe Info
 lookup_info infos id = Map.lookup id infos
 
 init_info :: ThreadId -> UUID.T -> Infos -> (Infos, ())
 init_info id uuid infos = (Map.insert id (Info uuid [] False Map.empty) infos, ())
 
 
 {- global state -}
 
 {-# NOINLINE global_state #-}
 global_state :: IORef Infos
 global_state = unsafePerformIO (newIORef Map.empty)
 
 find_id :: UUID.T -> IO (Maybe ThreadId)
 find_id uuid = do
   state <- readIORef global_state
   return $ fst <$> List.find (\(_, Info{uuid = uuid'}) -> uuid == uuid') (Map.assocs state)
 
 get_info :: ThreadId -> IO (Maybe Info)
 get_info id = do
   state <- readIORef global_state
   return $ lookup_info state id
 
 map_info :: ThreadId -> (Info -> Info) -> IO (Maybe Info)
 map_info id f =
   atomicModifyIORef' global_state
     (\infos ->
       case lookup_info infos id of
         Nothing -> (infos, Nothing)
         Just info ->
           let info' = f info
           in (Map.insert id info' infos, Just info'))
 
 delete_info :: ThreadId -> IO ()
 delete_info id =
   atomicModifyIORef' global_state (\infos -> (Map.delete id infos, ()))
 
 
 {- thread properties -}
 
 my_info :: IO (Maybe Info)
 my_info = do
   id <- Concurrent.myThreadId
   get_info id
 
 properties :: IO Properties.T
 properties = maybe [] props <$> my_info
 
 change_properties :: (Properties.T -> Properties.T) -> IO ()
 change_properties f = do
   id <- Concurrent.myThreadId
   map_info id (\info -> info {props = f (props info)})
   return ()
 
 
 {- managed resources -}
 
 add_resource :: IO () -> IO Unique
 add_resource resource = do
   id <- Concurrent.myThreadId
   u <- newUnique
   map_info id (\info -> info {resources = Map.insert u resource (resources info)})
   return u
 
 del_resource :: Unique -> IO ()
 del_resource u = do
   id <- Concurrent.myThreadId
   map_info id (\info -> info {resources = Map.delete u (resources info)})
   return ()
 
 bracket_resource :: IO () -> IO a -> IO a
 bracket_resource resource body =
   Exception.bracket (add_resource resource) del_resource (const body)
 
 
 {- stop -}
 
 is_stopped :: IO Bool
 is_stopped = maybe False stopped <$> my_info
 
 expose_stopped :: IO ()
 expose_stopped = do
   stopped <- is_stopped
   when stopped $ throw ThreadKilled
 
 stop :: ThreadId -> IO ()
 stop id = do
   info <- map_info id (\info -> info {stopped = True})
   let ops = case info of Nothing -> []; Just Info{resources} -> map snd (Map.toDescList resources)
   sequence_ ops
 
 
 {- UUID -}
 
 my_uuid :: IO (Maybe UUID.T)
 my_uuid = fmap uuid <$> my_info
 
 stop_uuid :: UUID.T -> IO ()
 stop_uuid uuid = do
   id <- find_id uuid
   forM_ id stop
 
 
 {- fork -}
 
 type Fork a = (ThreadId, UUID.T, IO (Result a))
 
 fork_finally :: IO a -> (Either SomeException a -> IO b) -> IO (Fork b)
 fork_finally body finally = do
   uuid <- UUID.random
   (id, result) <-
     Exception.mask (\restore ->
       Thread.forkIO
         (Exception.try
           (do
             id <- Concurrent.myThreadId
             atomicModifyIORef' global_state (init_info id uuid)
             restore body)
          >>= (\res -> do id <- Concurrent.myThreadId; delete_info id; finally res)))
   return (id, uuid, result)
 
 fork :: IO a -> IO (Fork a)
 fork body = fork_finally body Thread.result
 \<close>
 
 generate_file "Isabelle/Server.hs" = \<open>
 {-  Title:      Isabelle/Server.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 TCP server on localhost.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Server (
   localhost_name, localhost, publish_text, publish_stdout,
   server, connection
 )
 where
 
 import Control.Monad (forever, when)
 import qualified Control.Exception as Exception
 import Network.Socket (Socket)
 import qualified Network.Socket as Socket
 import qualified System.IO as IO
 import qualified Data.ByteString.Char8 as Char8
 
 import Isabelle.Library
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.UUID as UUID
 import qualified Isabelle.Byte_Message as Byte_Message
 import qualified Isabelle.Isabelle_Thread as Isabelle_Thread
 
 
 {- server address -}
 
 localhost_name :: Bytes
 localhost_name = "127.0.0.1"
 
 localhost :: Socket.HostAddress
 localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
 
 publish_text :: Bytes -> Bytes -> UUID.T -> Bytes
 publish_text name address password =
   "server " <> quote name <> " = " <> address <>
     " (password " <> quote (show_bytes password) <> ")"
 
 publish_stdout :: Bytes -> Bytes -> UUID.T -> IO ()
 publish_stdout name address password =
   Char8.putStrLn (Bytes.unmake $ publish_text name address password)
 
 
 {- server -}
 
 server :: (Bytes -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
 server publish handle =
   Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop)
   where
     open :: IO (Socket, Bytes)
     open = do
       server_socket <- Socket.socket Socket.AF_INET Socket.Stream Socket.defaultProtocol
       Socket.bind server_socket (Socket.SockAddrInet 0 localhost)
       Socket.listen server_socket 50
 
       port <- Socket.socketPort server_socket
       let address = localhost_name <> ":" <> show_bytes port
       password <- UUID.random
       publish address password
 
       return (server_socket, UUID.print password)
 
     loop :: Socket -> Bytes -> IO ()
     loop server_socket password = forever $ do
       (connection, _) <- Socket.accept server_socket
       Isabelle_Thread.fork_finally
         (do
           line <- Byte_Message.read_line connection
           when (line == Just password) $ handle connection)
         (\finally -> do
           Socket.close connection
           case finally of
             Left exn -> IO.hPutStrLn IO.stderr $ Exception.displayException exn
             Right () -> return ())
       return ()
 
 
 {- client connection -}
 
 connection :: String -> Bytes -> (Socket -> IO a) -> IO a
 connection port password client =
   Socket.withSocketsDo $ do
     addr <- resolve
     Exception.bracket (open addr) Socket.close body
   where
     resolve = do
       let hints =
             Socket.defaultHints {
               Socket.addrFlags = [Socket.AI_NUMERICHOST, Socket.AI_NUMERICSERV],
               Socket.addrSocketType = Socket.Stream }
       head <$> Socket.getAddrInfo (Just hints) (Just "127.0.0.1") (Just port)
 
     open addr = do
       socket <- Socket.socket (Socket.addrFamily addr) (Socket.addrSocketType addr)
                   (Socket.addrProtocol addr)
       Socket.connect socket $ Socket.addrAddress addr
       return socket
 
     body socket = do
       Byte_Message.write_line socket password
       client socket
 \<close>
 
 generate_file "Isabelle/Time.hs" = \<open>
 {-  Title:      Isabelle/Time.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Time based on milliseconds.
 
 See \<^file>\<open>~~/src/Pure/General/time.scala\<close>
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Time (
   Time, seconds, minutes, ms, zero, is_zero, is_relevant,
   get_seconds, get_minutes, get_ms, message
 )
 where
 
 import Text.Printf (printf)
 import Isabelle.Bytes (Bytes)
 import Isabelle.Library
 
 
 data Time = Time Int
 
 instance Eq Time where Time ms1 == Time ms2 = ms1 == ms2
 instance Ord Time where compare (Time ms1) (Time ms2) = compare ms1 ms2
 
 seconds :: Double -> Time
 seconds s = Time (round (s * 1000.0))
 
 minutes :: Double -> Time
 minutes m = Time (round (m * 60000.0))
 
 ms :: Int -> Time
 ms = Time
 
 zero :: Time
 zero = ms 0
 
 is_zero :: Time -> Bool
 is_zero (Time ms) = ms == 0
 
 is_relevant :: Time -> Bool
 is_relevant (Time ms) = ms >= 1
 
 get_seconds :: Time -> Double
 get_seconds (Time ms) = fromIntegral ms / 1000.0
 
 get_minutes :: Time -> Double
 get_minutes (Time ms) = fromIntegral ms / 60000.0
 
 get_ms :: Time -> Int
 get_ms (Time ms) = ms
 
 instance Show Time where
   show t = printf "%.3f" (get_seconds t)
 
 message :: Time -> Bytes
 message t = make_bytes (show t) <> "s"
 \<close>
 
 generate_file "Isabelle/Timing.hs" = \<open>
 {-  Title:      Isabelle/Timing.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Support for time measurement.
 
 See \<^file>\<open>~~/src/Pure/General/timing.ML\<close>
 and \<^file>\<open>~~/src/Pure/General/timing.scala\<close>
 -}
 
 module Isabelle.Timing (
   Timing (..), zero, is_zero, is_relevant
 )
 where
 
 import qualified Isabelle.Time as Time
 import Isabelle.Time (Time)
 
 data Timing = Timing {elapsed :: Time, cpu :: Time, gc :: Time}
   deriving (Show, Eq)
 
 zero :: Timing
 zero = Timing Time.zero Time.zero Time.zero
 
 is_zero :: Timing -> Bool
 is_zero t = Time.is_zero (elapsed t) && Time.is_zero (cpu t) && Time.is_zero (gc t)
 
 is_relevant :: Timing -> Bool
 is_relevant t = Time.is_relevant (elapsed t) || Time.is_relevant (cpu t) || Time.is_relevant (gc t)
 \<close>
 
 generate_file "Isabelle/Bash.hs" = \<open>
 {-  Title:      Isabelle/Bash.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Support for GNU bash.
 
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/System/bash.ML\<close>
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Bash (
   string, strings,
 
   Params,
   get_script, get_input, get_cwd, get_putenv, get_redirect,
   get_timeout, get_description,
   script, input, cwd, putenv, redirect, timeout, description,
 )
 where
 
 import Text.Printf (printf)
 import qualified Isabelle.Symbol as Symbol
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Time as Time
 import Isabelle.Time (Time)
 import Isabelle.Library
 
 
 {- concrete syntax -}
 
 string :: Bytes -> Bytes
 string str =
   if Bytes.null str then "\"\""
   else str |> Bytes.unpack |> map trans |> Bytes.concat
     where
       trans b =
         case Bytes.char b of
           '\t' -> "$'\\t'"
           '\n' -> "$'\\n'"
           '\f' -> "$'\\f'"
           '\r' -> "$'\\r'"
           c ->
             if Symbol.is_ascii_letter c || Symbol.is_ascii_digit c || c `elem` ("+,-./:_" :: String)
             then Bytes.singleton b
             else if b < 32 || b >= 127 then make_bytes (printf "$'\\x%02x'" b :: String)
             else "\\" <> Bytes.singleton b
 
 strings :: [Bytes] -> Bytes
 strings = space_implode " " . map string
 
 
 {- server parameters -}
 
 data Params = Params {
     _script :: Bytes,
     _input :: Bytes,
     _cwd :: Maybe Bytes,
     _putenv :: [(Bytes, Bytes)],
     _redirect :: Bool,
     _timeout :: Time,
     _description :: Bytes}
   deriving (Show, Eq)
 
 get_script :: Params -> Bytes
 get_script = _script
 
 get_input :: Params -> Bytes
 get_input = _input
 
 get_cwd :: Params -> Maybe Bytes
 get_cwd = _cwd
 
 get_putenv :: Params -> [(Bytes, Bytes)]
 get_putenv = _putenv
 
 get_redirect :: Params -> Bool
 get_redirect = _redirect
 
 get_timeout :: Params -> Time
 get_timeout = _timeout
 
 get_description :: Params -> Bytes
 get_description = _description
 
 script :: Bytes -> Params
 script script = Params script "" Nothing [] False Time.zero ""
 
 input :: Bytes -> Params -> Params
 input input params = params { _input = input }
 
 cwd :: Bytes -> Params -> Params
 cwd cwd params = params { _cwd = Just cwd }
 
 putenv :: [(Bytes, Bytes)] -> Params -> Params
 putenv putenv params = params { _putenv = putenv }
 
 redirect :: Params -> Params
 redirect params = params { _redirect = True }
 
 timeout :: Time -> Params -> Params
 timeout timeout params = params { _timeout = timeout }
 
 description :: Bytes -> Params -> Params
 description description params = params { _description = description }
 \<close>
 
 generate_file "Isabelle/Process_Result.hs" = \<open>
 {-  Title:      Isabelle/Process_Result.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Result of system process.
 
 See \<^file>\<open>~~/src/Pure/System/process_result.ML\<close>
 and \<^file>\<open>~~/src/Pure/System/process_result.scala\<close>
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Process_Result (
   interrupt_rc, timeout_rc,
 
   T, make, rc, out_lines, err_lines, timing, timing_elapsed, out, err, ok, check
 )
 where
 
 import Isabelle.Time (Time)
 import qualified Isabelle.Timing as Timing
 import Isabelle.Timing (Timing)
 import Isabelle.Bytes (Bytes)
 import Isabelle.Library
 
 
 interrupt_rc :: Int
 interrupt_rc = 130
 
 timeout_rc :: Int
 timeout_rc = 142
 
 data T =
   Process_Result {
     _rc :: Int,
     _out_lines :: [Bytes],
     _err_lines :: [Bytes],
     _timing :: Timing}
   deriving (Show, Eq)
 
 make :: Int -> [Bytes] -> [Bytes] -> Timing -> T
 make = Process_Result
 
 rc :: T -> Int
 rc = _rc
 
 out_lines :: T -> [Bytes]
 out_lines = _out_lines
 
 err_lines :: T -> [Bytes]
 err_lines = _err_lines
 
 timing :: T -> Timing
 timing = _timing
 
 timing_elapsed :: T -> Time
 timing_elapsed = Timing.elapsed . timing
 
 out :: T -> Bytes
 out = trim_line . cat_lines . out_lines
 
 err :: T -> Bytes
 err = trim_line . cat_lines . err_lines
 
 ok :: T -> Bool
 ok result = rc result == 0
 
 check :: T -> T
 check result = if ok result then result else error (make_string $ err result)
 \<close>
 
 generate_file "Isabelle/Options.hs" = \<open>
 {-  Title:      Isabelle/Options.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 System options with external string representation.
 
 See \<^file>\<open>~~/src/Pure/System/options.ML\<close>
 and \<^file>\<open>~~/src/Pure/System/options.scala\<close>
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE InstanceSigs #-}
 
 module Isabelle.Options (
   boolT, intT, realT, stringT, unknownT,
 
   T, typ, bool, int, real, seconds, string,
   decode
 )
 where
 
 import qualified Data.Map.Strict as Map
 import Data.Map.Strict (Map)
 import qualified Isabelle.Properties as Properties
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Value as Value
 import qualified Isabelle.Time as Time
 import Isabelle.Time (Time)
 import Isabelle.Library
 import qualified Isabelle.XML.Decode as Decode
 import Isabelle.XML.Classes (Decode (..))
 
 
 {- representation -}
 
 boolT :: Bytes
 boolT = "bool"
 
 intT :: Bytes
 intT = "int"
 
 realT :: Bytes
 realT = "real"
 
 stringT :: Bytes
 stringT = "string"
 
 unknownT :: Bytes
 unknownT = "unknown"
 
 data Opt = Opt {
   _pos :: Properties.T,
   _name :: Bytes,
   _typ :: Bytes,
   _value :: Bytes }
 
 data T = Options (Map Bytes Opt)
 
 
 {- check -}
 
 check_name :: T -> Bytes -> Opt
 check_name (Options map) name =
   case Map.lookup name map of
     Just opt | _typ opt /= unknownT -> opt
     _ -> error (make_string ("Unknown system option " <> quote name))
 
 check_type :: T -> Bytes -> Bytes -> Opt
 check_type options name typ =
   let
     opt = check_name options name
     t = _typ opt
   in
     if t == typ then opt
     else error (make_string ("Ill-typed system option " <> quote name <> " : " <> t <> " vs. " <> typ))
 
 
 {- get typ -}
 
 typ :: T -> Bytes -> Bytes
 typ options name = _typ (check_name options name)
 
 
 {- get value -}
 
 get :: Bytes -> (Bytes -> Maybe a) -> T -> Bytes -> a
 get typ parse options name =
   let opt = check_type options name typ in
     case parse (_value opt) of
       Just x -> x
       Nothing ->
         error (make_string ("Malformed value for system option " <> quote name <>
           " : " <> typ <> " =\n" <> quote (_value opt)))
 
 bool :: T -> Bytes -> Bool
 bool = get boolT Value.parse_bool
 
 int :: T -> Bytes -> Int
 int = get intT Value.parse_int
 
 real :: T -> Bytes -> Double
 real = get realT Value.parse_real
 
 seconds :: T -> Bytes -> Time
 seconds options = Time.seconds . real options
 
 string :: T -> Bytes -> Bytes
 string = get stringT Just
 
 
 {- decode -}
 
 instance Decode T where
   decode :: Decode.T T
   decode =
     let
       decode_entry :: Decode.T (Bytes, Opt)
       decode_entry body =
         let
           (pos, (name, (typ, value))) =
             Decode.pair Decode.properties (Decode.pair Decode.string (Decode.pair Decode.string Decode.string)) body
         in (name, Opt { _pos = pos, _name = name, _typ = typ, _value = value })
     in Options . Map.fromList . Decode.list decode_entry
 \<close>
 
 export_generated_files _
 
 end