more direct HTML presentation, without print mode;

tuned signature;

more explicit markup for improper commands;
clarified CSS rendering;

imitate command markup and rendering of Isabelle/jEdit in HTML output;

more abstract type Input.source;

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

more explicit Keyword.keywords;

recover via scanner;
tuned signature;

separate module Command_Span: mostly syntactic representation;
potentially prover-specific Output_Syntax.parse_spans;

clarified Command_Span in accordance to Scala (see also c2c1e5944536);

more explicit type Span in Scala, according to ML version;

tuned signature;

suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
tuned signature;

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";

clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
tuned message;

tuned signature;

clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;

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

release file errors at runtime: Command.eval instead of Command.read;

tuned signature;

clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer);
simplified command padding: always newline, despite lack of indentation;

clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
clarified unknown timing vs. zero timing;
tuned;

more Thy_Syntax.element operations;

simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
eliminated separate Outer_Syntax.read_element;

tuned;

support nested Thy_Syntax.element;
more explicit Keyword.is_proof_body;
tuned;

more uniform Symbol.is_ascii_identifier in ML/Scala;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

tuned errors;

some support for inlining file content into outer syntax token language;

tuned;

more liberal scanning of potentially malformed symbols;

clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);

sneak message into "bad" markup as property -- to be displayed after YXML parsing;

discontinued mostly unused markup for command spans;

more visible markup of malformed input as "bad";

some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;

clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
simplified signatures;

separate module for concrete Isabelle markup;

--HG--
rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML
rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala

bulk reports for improved message throughput;

eliminated markup for plain identifiers (frequent but insignificant);
reduced "black" markup (outer string etc. takes care of it already);

more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;

tuned;

discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;

clarified Thy_Syntax.element;

more uniform treatment of "keyword" vs. "operator";

discontinued special treatment of structure Lexicon;

more direct treatment of Position.end_offset;
tuned;

eliminated obsolete Token.Malformed -- subsumed by Token.Error;

report malformed symbols;

simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing;
refined treatment of malformed surrogates (Scala);

support for floating-point tokens in outer syntax (coinciding with inner syntax version);

explicitly qualify type Output.output, which is a slightly odd internal feature;

tuned signature of (Context_)Position.report variants;

uniform Markup.empty/Markup.Empty in ML and Scala;

report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;

rename "unit" to "atom", to avoid confusion with the unit type;

modernized some structure names, keeping a few legacy aliases;

more detailed token markup, including command kind as sub_kind;
type-safe access to Command.HighlightInfo;

simplified command/keyword markup;

markup non-identifier keyword as operator;

renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
eliminated slightly odd alias structure T;

--HG--
rename : src/Pure/Isar/outer_lex.ML => src/Pure/Isar/token.ML

refer directly to structure Keyword and Parse;
eliminated old-style structure aliases K and P;

de-camelized Symbol_Pos;

more detailed inner token markup;

renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);

--HG--
rename : src/Pure/Thy/thy_edit.ML => src/Pure/Thy/thy_syntax.ML