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

support for dynamic document output while editing;

tuned: prefer list operations over Source.source;

clarified operations;

discontinued old form of marginal comments;

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

tuned signature;

more symbols;

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

tuned;

prefer hybrid 'bundle' command;

more IDE support for Isabelle/Pure bootstrap;

clarified modules -- simplified bootstrap;

clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;

more thorough check_command, including completion;

symbolic syntax "\<comment> text";

tuned signature, in accordance to sortBy in Scala;

more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;

tuned according to a81dc82ecba3;

more explicit bootstrap_thy;
clarified error;

more robust error handling of commands that are declared but not yet defined;

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;

clarified command keyword markup;

support local command setup;

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;

support private scope for individual local theory commands;
tuned signature;

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;

prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
tuned message;

tuned signature;

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;

simplified keyword kinds;
more explicit bootstrap syntax;

tuned signature;

eliminated pointless dynamic keywords (TTY legacy);

explicit type Keyword.keywords;
tuned signature;

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

recover via scanner;
tuned signature;

simplified -- scanning is never interactive;

tuned signature, in accordance to Scala version;

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

discontinued obsolete \<^sync> marker;

discontinued obsolete tty and prompt;

tuned signature according to Scala version -- prefer explicit argument;

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

more markup;

tuned signature;

afford strict check (see also AFP/a8e08d947f0a);

tuned message;

discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;

some shortcuts for chunks, which sometimes avoid bulky string output;

prefer Context_Position where a context is available;
prefer explicit Context_Position.is_visible -- avoid redundant message composition;
tuned signature;

clarified bootstrap process: switch to ML with context and antiquotations earlier;

tuned signature;

tuned message;

explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;

clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;

tuned signature;

tuned signature;

tuned signature -- agree with markup terminology;

tuned comment;

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

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

generalized notion of active area, where sendback is just one application;
some support for graphview via active area;

--HG--
rename : src/Pure/PIDE/sendback.ML => src/Pure/PIDE/active.ML
rename : src/Tools/jEdit/src/sendback.scala => src/Tools/jEdit/src/active.scala

more general sendback properties;
support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';

refined outer syntax 'help' command;

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

tuned;

renamed Position.str_of to Position.here;

check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);

added keyword kind "thy_load" (with optional list of file extensions);

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

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

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

report commands as formal entities, with def/ref positions;

more official command specifications, including source position;

more standard bootstrapping of Pure.thy;

internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;

static relevance of proof via syntax keywords;

allow keyword tags to be redefined, but not the command category;

check declared vs. defined commands at end of session;

outer syntax command definitions based on formal command_spec derived from theory header declarations;

define keywords early when processing the theory header, before running the body commands;

clarified Keyword.is_keyword: union of minor and major;
misc tuning and simplification;

declare command keywords via theory header, including strict checking outside Pure;

refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);

bulk reports for improved message throughput;

tuned;

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

tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;

tuned Parse.group: delayed failure message;

simplified Toplevel.init_theory: discontinued special name argument;

simplified Toplevel.init_theory: discontinued special master argument;

moved Outer_Syntax.load_thy to Thy_Load.load_thy;
tuned signatures;
tuned module dependencies;

less stateful outer_syntax;

clarified Thy_Syntax.element;

present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;

structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;

more tracing information via Par_List.map_name;

Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;

more direct treatment of Position.end_offset;
tuned;

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

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

Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
some partial workarounds for Cygwin;

explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);

simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database;
Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command;
added Thy_Load.begin_theory for clarity;
structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader;
moved some basic commands from isar_cmd.ML to isar_syn.ML;
misc tuning and simplification;

simplified handling of theory begin/end wrt. toplevel and theory loader;

load_thy: parallel parsing of units, which consist of statement/proof each;

deps_thy/load_thy: store compact text to reduce space by factor 12;

eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
misc tuning and simplification;

eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
tuned some error messages;

Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;

modernized some structure names, keeping a few legacy aliases;

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

centralized legacy aliases;

renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;

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

non-critical atomic accesses;

explicit indication of Unsynchronized.ref;

de-camelized Symbol_Pos;

eliminated type Args.T;
pervasive types 'a parser and 'a context_parser;

load_thy: explicit after_load phase for presentation;

added local_theory';

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

added type 'a parser, simplified signature;
added internal_command wrapper;
tuned;

load_thy: more precise treatment of improper cmd or proof (notably 'oops');

load_thy: Toplevel.excursion based on units of command/proof pairs;

simplified process_file, eliminated Toplevel.excursion;
load_thy: separation of Toplevel.command_excursion and ThyOutput.present_thy (intermediate state persist until commit_exit);

P.doc_source and P.ml_sorce for proper SymbolPos.text;

load_thy: no untabify (preserve position information!), present spans instead of verbatim source;

Symbol.source/OuterLex.source: more explicit do_recover argument;
scan: pass position;
removed obsolete prepare_command (now inlined in isar_syn.ML);
renamed prepare_command_failsafe to prepare_command, reports tokens;
load_thy: now based on ThyEdit operations, reports tokens and spans;
tuned;

Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;

updated type of nested sources;

simplified prepare_command;

renamed IsarCmd.nested_command to OuterSyntax.prepare_command;

adapted IsarCmd.init_theory;

Toplevel.init_theory: pass name explicitly;

moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;

added local_theory command wrappers;

renamed Position.path to Path.position;

Pretty.mark;

eliminated unused trace, read;

export load_thy -- no backpatching;

moved structure Isar to isar.ML;
added type isar (from toplevel.ML);

added process_file;

adapted to Context.thread_data interface;

theory loader: discontinued *attached* ML scripts;

tuned messages;

secure_main: removed separate welcome;

try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;

cond_timeit: added message argument;

secure_main: enforces terminator, to gain robustness;

added off-line parse;
read: no recovery on non-interactive source, yields proper errors;

added Isar.secure_main;
pass Secure.is_secure to Toplevel.loop;

report on keyword/command declarations;
tuned;

simplified interfaces for outer syntax;
tuned;

load_thy: try_ml_file unconditionally;

marked some CRITICAL sections;

load_thy: avoid reloading of text;
tuned;

marked some CRITICAL sections;

simplified ThyLoad interfaces: only one additional directory;

moved deps_thy to ThyLoad (independent of outer syntax);
tuned load_thy;

exported command_keyword;
tuned;

export get_lexicons;

nested source: explicit interactive flag for recover avoids duplicate errors;

toplevel_source: interactive flag indicates intermittent error_msg;
nested source: error msg passed to recover;
tuned source positions;

explicit treatment of legacy_features;

renamed IsarOutput to ThyOutput;
tuned Scan.extend_lexicon;
moved ML context stuff to from Context to ML_Context;

adapted ML context operations;

refrain from setting ml_prompts again;

Toplevel.init_state;

avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

prefer Proof.context over Context.generic;

added Isar.goal;

Isar.context: proper error;

removed OldGoals.legacy flag (always warn);
added warning for legacy ML scripts;

added Isar.context;

tuned basic list operators (flat, maps, map_filter);

check_text: Toplevel.node option;

run_thy: removed Output.toplevel_errors;

added Isar.toplevel;

tuned msg;

added Isar.state/exn;

load_file: setmp OldGoals.legacy true;

removed old-style theory format;
tuned;

TableFun/Symtab: curried lookup and update;

tuned msg;

tuned check_text;

tuned msg;

deprecated non-Isar theory file format;

curried_lookup/update;

use AList operations;

fixed command prompt (was broken due to P.tags);

moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
support for tagged commands;
tuned theory presentation interface;

Inttab.defined;

dest_parsers: sort result;

tuned;

re-init ml_prompts after loop termination;

tuned;

added structure Isar (from isar.ML);

Move towards standard functions.

Deleted Library.option type.

Allow scanning to recover and reconstruct bad input

Adapted to new interface of function ThyLoad.check_file

Remove isar_readstring. Split read into scanner and parser.

Merged in license change from Isabelle2004

removed unused help function;

added read (provides transition names and sources);

added is_keyword;

A patch by david aspinall

added check_text;

got rid of explicit marginal comments (now stripped earlier from input);

recover: ignore result;

added thy_script kind;

prf_heading kind;

removed help;
added print_commands;

help_antiquotations;

moved header stuff to thy_header.ML;
moved theory presentation to isar_output.ML;
major cleanup;

prf_open/close;

do not setmp Library.timing;

improved terminator msg;

global timing flag;

GPLed;

Pretty.chunks;

support markup environments;

presentation ignore stuff: swallow newline;

ignore_stuff;
P.!!!!;

added K.qed_global;

Present.old_symbol_source;

fixed error msg;

improved ml handling;

markup: keep indentation;

old_header: proper error message;

verbatim markup tokens;

Present.token_source after load (better errors!?);

present source *before* theory load;

improved present_token;

added markup_command;

simplified;
header command;

present token source;

export token_source;
improved Present.theory_source;

added prf_asm_goal;

help: unknown theory context;

tuned;

print_help;

isar: no_pos flag;

ThyInfo.may_load_file;

removed warn_theory_style;

simplified ML handling;

added thy_switch kind;

Toplevel.excursion_error;

separate command tokens;

added prf_asm;

added sync;

qed_block keywords;

added keyword classification;

tuned;

rearranged some modules;

added (improper_)command;

Present.theory_source;

more robust handling of theory context;
header-only theory files;

leave theory context after load_thy;

made SML/NJ happy;

removed load;
detect old vs. new header;
provide deps_thy, load_thy primitives for ThyLoad;

tuned msg;

tuned msg;

tuned welcome msg;

added commands;

load;

tuned names;

The global Isabelle/Isar outer syntax.