shortlogentry/filelogentry: show shortdate and full description;

Removed uses of context element includes.

added Isar.command, Isar.insert, Isar.remove (editor model);

export type id with no_id and create_command; basic support for editor model: insert_command, remove_command; refined command status; misc tuning;

tuned;

renamed IsarCmd.nested_command to OuterSyntax.prepare_command;

load thy_edit.ML before isar.ML;

modernized specifications and proofs; tuned document;

Removed uses of context element includes.

tuned

tuned code theorem bookkeeping

tuned changelogentry;

refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);

support for command status;

added status channel; writeln_default: suppress empty messages;

added status channel;

tuned;

simplified commit_exit;

simplified commit_exit: operate on previous node of final state, include warning here; misc tuning;

removed obsolete commit_exit;

added command 'linear_undo'; tuned;

removed command 'redo'; added command 'linear_undo';

adapted ThyInfo.end_theory;

dropped map; fixed swap

curried gcd

cover macbroy as well; tuned;

tuned filelogentry;

print_mode "test_markup": do not change prompt, otherwise Proof General will not work;

tuned message;

updated generated file;