isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);

clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);

clarified signature;

proper datatype for 8-bit characters

updated to 146757999c8d;

embedded content may be delimited via cartouches;

misc tuning and modernization;

explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
handle bootstrap signatures as well;

clarified conditional compilation;

model characters directly as range 0..255
* * *
operate on syntax terms rather than asts

isabelle update_cartouches -c -t;

clarified Antiquote.antiq_reports;
Thy_Output.output_text: support for markdown (inactive);
eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;

prefer tactics with explicit context;

@{command_spec} is superseded by @{command_keyword};

tuned signature;

explicit message channels for "state", "information";
separate state_message_color;

tuned;

more examples;

expand ML cartouches to Input.source;
tuned signature;

tuned header;

update_cartouches;

tuned signature;

more abstract type Input.source;

tuned signature;

uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
discontinued obsolete 'txt_raw' (superseded by 'text_raw');
eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds);
'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind;
changed tagging of diagnostic commands within proof;

more careful ML source positions, for improved PIDE markup;

more position information, e.g. relevant for errors in generated ML source;

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

modernized header uniformly as section;

proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);

allow text cartouches in regular outer syntax categories "text" and "altstring";

redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
more explicit ML_Compiler.flags;

separate tokenization and language context for SML: no symbols, no antiquotes;

added command 'SML_file' for Standard ML without Isabelle/ML add-ons;

tuned signature -- clarified module name;

--HG--
rename : src/Pure/ML/ml_antiquote.ML => src/Pure/ML/ml_antiquotation.ML

clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";

simplified inner syntax;

avoid breakdown of document preparation, which does not understand cartouche tokens yet;

more cartouche examples, including uniform nesting of sub-languages;

implicit "cartouche" method (experimental, undocumented);

more examples;

proper \<newline>;

support for nested text cartouches;
clarified Symbol.is_symbolic: exclude \<open> and \<close>;