args: explicit groups for file_name, theory_name;

read_asts: Lexicon.report_token, filter Lexicon.is_proper; report tokens;

filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;

token_kind: add Space, Comment; tokenize: now includes improper tokens, cf. is_proper; added report_token;

renamed T.source_of' to T.source_position_of; tuned signature;

renamed T.source_of' to T.source_position_of;

output_markup: check Markup.is_none;

added is_none; added inner_comment;

Args.name_source(_position) for proper position information;

[source=false] for quoted antiquotation avoids quote-escapes in output;

report antiquotations;

tuned;

report ML_source;

renamed P.ml_source to P.ML_source;

report doc_source;

added ML_source, doc_source;

antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;

added source_of';

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

oracle, header/local_theory/proof_markup: pass SymbolPos.text;

use SymbolPos.T list directly, instead of encoded SymbolPos.text;

ML_Context.add_antiq: pass position; @{lemma}: set source position;

ML_Context.add_antiq: pass position;

retrieve_thms: transfer fact position to result; tuned;

moved basic thm operations from structure PureThy to Thm; added position operations; tuned;

moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);

made SML/NJ happy;

removed obsolete present_html -- now part of regular theory presentation;