2009-01-16 wenzelm 2009-01-16 define_state: use empty_state; edit_document: report_updates before running commands; tuned;
2009-01-16 wenzelm 2009-01-16 provide end_document;
2009-01-16 wenzelm 2009-01-16 run command: check theory name for init; tuned;
2009-01-16 wenzelm 2009-01-16 fold_entries: non-optional start, permissive; renamed find_entries to first_entry, tuned; update_state: run as state_id'; update_states: symmetric changes;
2009-01-15 wenzelm 2009-01-15 command 'Isar.edit_document': actually invoke edit_document;
2009-01-15 wenzelm 2009-01-15 tuned;
2009-01-15 wenzelm 2009-01-15 edit_document: proper edits/edit markup, including the document id; tuned;
2009-01-15 wenzelm 2009-01-15 removed junk;
2009-01-15 wenzelm 2009-01-15 misc cleanup and simplification;
2009-01-13 wenzelm 2009-01-13 misc internal rearrangements; fold_entries: really start from start, or optional position; added find_first_entries, find_first_entries; insert_entry: always invalidate next state; added refresh_states (partial version);
2009-01-13 wenzelm 2009-01-13 replaced sys_error by plain error; some basic operations on command entries within a document;
2009-01-13 wenzelm 2009-01-13 added Isar/isar_document.ML: Interactive Isar documents.