updated

set printmode while marking

updated

avoid reference to theory Ferrack altogether

more canonical theory setup

set depth to 1

avoid theory Imperative_HOL altogether

adapted to change eq -> equal

corrected printmode handling

swapped slip

updated

restored and added surpression of case combinators

dropped superfluous presentation names

manage statement selection for presentation wholly through markup

formal markup of generated code for statements

removed namespace stuff from code_printer

merged

reenable Nitpick on Cygwin; we'll see tomorrow if there's still a failure, and if so I'll investigate

merged;

Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";

turned show_consts into proper configuration option;

prefer regular Proof.context over background theory; misc tuning and simplification;

just one refute.ML;

use existing Integer.pow, despite its slightly odd argument order;

tuned whitespace and indentation, emphasizing the logical structure of this long text;

inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;

Document_View: squiggly underline for messages; tuned;

added gfx_range convenience;

Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;

Position.Range: exclude singularity (again);