document markers are formal comments, and may thus occur anywhere in the command-span;
clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure;
tuned signature;

clarified signature;
more thorough end_pos;

tuned signature;

clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;

markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);

adjust position according to offset of command/exec id;

clarified signature;

clarified signature;

tuned message;

clarified operations;

tuned signature: removed unused operations;

clarified signature;

clarified operations;

discontinued old form of marginal comments;

clarified markup;

more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;

more markup for HTML rendering;

tuned signature;

more HTML rendering as in Isabelle/jEdit;
tuned;

avoid extra decorations for regular command keywords;

more uniform treatment of "bad" like other messages (with serial number);

more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;

discontinued raw symbols;
discontinued Symbol.source;
use initial Symbol.explode;

print name in parsable form;

prefer internal attribute source;

eliminated "xname" and variants;

tuned signature;

tuned;

tuned signature;

clarified modules;

prefer non-ASCII output;

make SML/NJ happy;

tuned;

tuned signature;

tuned;

clarified type Token.src: plain token list, with usual implicit value assignment;
clarified type Token.name_value, notably for head of Token.src;
clarified Attrib/Method check_src vs. parser;

added document antiquotation @{theory_text};
tuned document;

tuned signature;

support control symbol antiquotations;

moved remaining display.ML to more_thm.ML;

trim context more thoroughly;

clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);

support for 'restricted' modifier: only qualified accesses outside the local scope;

more general notion of command span: command keyword not necessarily at start;
support for special 'private' prefix for local_theory commands;
clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;

tuned signature;

operation on embedded sources for Eisbach;

tuned -- emphasize semantics of already checked src;

clarified input source;

tuned signature;

clarified Token.check_src: intern at most once;
Method.parse_internal for Eisbach: intern method names;

added declare_maxidx operations for Eisbach;

more explicit markup for improper commands;
clarified CSS rendering;

tuned;

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

expand ML cartouches to Input.source;
tuned signature;

clarified define_command: send tokens more directly, without requiring keywords in ML;

tuned signature;

clarified token kind;

more abstract type Input.source;

modifier markup for all parsed tokens;
report literal token markup, before re-assignment;

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

eliminated pointless dynamic keywords (TTY legacy);

explicit type Keyword.keywords;
tuned signature;

tuned signature (see ab2483fad861);

recover via scanner;
tuned signature;

simplified -- scanning is never interactive;

command-line terminator ";" is no longer accepted;

removed pointless markup;
tuned comments;

discontinued obsolete \<^sync> marker;

discontinued obsolete tty and prompt;

tuned signature;

tuned;

support for declaration within token source;

support for nested Token.src within Token.T;
tuned signature;

tuned signature -- moved type src to Token, without aliases;

more informative Token.Name with history of morphisms;
tuned signature;

more informative Token.Fact: retain name of dynamic fact (without selection);

more markup for improper elements;

clarified Markup.operator vs. Markup.delimiter;
tuned color;

more explicit markup for Token.Literal;
Markup.quasi_keyword for Parse.$$$ -- it is used within Args.syntax as well;
Markup.operator for name of Args.syntax, to override outer keywords like "where";
tuned signature;

more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;

more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;

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

clarified init_assignable: make double-sure that initial values are reset;
more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";

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

store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
integrity check of SHA1 digests produced in Scala vs. ML;
tuned signature;

back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;

tuned message -- more markup;

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

clarified Token.range_of in accordance to Symbol_Pos.range;
eliminated redundant Position.set_range, which is already included in Position.range;

tuned signature;

tuned signature;

tuned signature;

tuned error messages, more accurate position;

tuned -- more direct err_prefix;

clarified scan_cartouche_depth, according to Scala version;
more accurate error position;

tuned errors;

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

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

maintain blobs within document state: digest + text in ML, digest-only in Scala;
resolve files for command span, based on defined blobs;
tuned;

unified Command.is_proper in ML with Scala (see also 123be08eed88);

tuned signature;
tuned;

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

more proof method text position information;

renamed Position.str_of to Position.here;

tuned messages: end-of-input rarely means physical end-of-file from the past;

clarified type Token.file;

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

clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;

proper error prefixes;

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

refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;

tuned signature;

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

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

defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);

more precise Symbol_Pos.quote_string;

inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
tuned signature;

discontinued special treatment of hard tabulators;

more uniform variations of scan_string;

discontinued special treatment of structure Lexicon;

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

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;

eliminated slightly odd pervasive Symbol_Pos.symbol;

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

more robust treatment of Markup.token;

simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;

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