removed final periods in messages for proof methods

tuned proofs;

added a version of the Metis tactic that returns the unused facts

tuned code

more NEWS

folded 'Option.set' into BNF-generated 'set_option'

merged

prefer user-space tool within Pure.thy;

more markup;

more uniform rendering of text that is formally interpreted: avoid clash with inner markup;

recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;

support ML antiquotations in Scala; tuned -- more uniform ML vs. Scala;

antiquotations within plain text: Scala version in accordance to ML;

tuned signature -- emphasize line-oriented aspect;

eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)

tuned whitespace;

removed odd comments -- inferred types are shown by Prover IDE;

removed dead code; tuned;

more uniform ML keyword markup; tuned;

merged

tuned;

clarified Isabelle/ML strings;

refined ML keyword styles;

isabelle-ml mode with separate token marker; clarified ML_Lex.gap_start: end-of-input counts as single newline;

partial scans via ML_Lex.tokenize_context; simplified ML_char: no gaps (hardly relevant in practice); tuned;

proper signature; removed dead code;

lexical syntax for SML (in Scala); tuned;

tuned;

removed dead code;

tuned signature (in accordance to ML version);