src/Pure/Isar/outer_syntax.scala
19 months ago wenzelm 2017-10-07 clarified empty merge; tuned;
19 months ago wenzelm 2017-09-29 more informative loaded_theories: dependencies and syntax;
2017-04-04 wenzelm 2017-04-04 more explicit types;
2017-04-04 wenzelm 2017-04-04 proper name according to meaning;
2016-12-20 wenzelm 2016-12-20 tuned;
2016-09-14 wenzelm 2016-09-14 maintain abbrevs in canonical reverse order;
2016-09-14 wenzelm 2016-09-14 tuned;
2016-08-04 wenzelm 2016-08-04 clarified modules;
2016-08-04 wenzelm 2016-08-04 clarified modules;
2016-08-03 wenzelm 2016-08-03 include 'begin' and 'end' structure in text folds;
2016-08-02 wenzelm 2016-08-02 implicit keyword completion only for actual words (amending 73939a9b70a3);
2016-08-02 wenzelm 2016-08-02 tuned signature -- prover-independence is presently theoretical;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-07-20 wenzelm 2016-07-20 completion templates for commands involving "begin ... end" blocks;
2016-07-13 wenzelm 2016-07-13 tuned;
2016-07-12 wenzelm 2016-07-12 clarified;
2016-07-12 wenzelm 2016-07-12 clarified;
2016-07-12 wenzelm 2016-07-12 closing 'qed' or '}' is outside of fold;
2016-07-11 wenzelm 2016-07-11 explicit kind "before_command"; tuned signature;
2016-07-10 wenzelm 2016-07-10 tuned signature: more uniform Keyword.spec;
2016-07-07 wenzelm 2016-07-07 clarified signature;
2016-02-28 wenzelm 2016-02-28 discontinued old 'header';
2016-01-24 wenzelm 2016-01-24 proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;
2015-10-17 wenzelm 2015-10-17 added 'paragraph', 'subparagraph';
2015-07-08 wenzelm 2015-07-08 clarified text folds: proof ... qed counts as extra block;
2015-07-08 wenzelm 2015-07-08 tuned;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 wenzelm 2015-04-04 more general notion of command span: command keyword not necessarily at start; support for special 'private' prefix for local_theory commands; clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;
2015-03-17 wenzelm 2015-03-17 misc tuning and simplification;
2015-03-15 wenzelm 2015-03-15 hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;
2015-03-15 wenzelm 2015-03-15 more command categories, as in ML;
2015-03-12 wenzelm 2015-03-12 clarified command content;
2015-01-08 wenzelm 2015-01-08 tuned;
2014-12-09 wenzelm 2014-12-09 tuned signature;
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-12-02 wenzelm 2014-12-02 node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;
2014-12-01 wenzelm 2014-12-01 more merge operations;
2014-11-07 wenzelm 2014-11-07 tuned outline;
2014-11-05 wenzelm 2014-11-05 more uniform header_keywords in ML/Scala; tuned signature;
2014-11-05 wenzelm 2014-11-05 clarified representation of type Keywords; tuned signature;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.Keywords;
2014-11-05 wenzelm 2014-11-05 clarified minor/major lexicon (like ML version);
2014-11-02 wenzelm 2014-11-02 uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete control command category;
2014-10-21 wenzelm 2014-10-21 tuned;
2014-10-21 wenzelm 2014-10-21 support for structure matching; misc tuning;
2014-10-21 wenzelm 2014-10-21 tuned rendering;
2014-10-21 wenzelm 2014-10-21 clarified tree root;
2014-10-19 wenzelm 2014-10-19 tuned signature and modules;
2014-10-18 wenzelm 2014-10-18 more folds;
2014-10-18 wenzelm 2014-10-18 clarified Line_Structure wrt. command span;
2014-10-18 wenzelm 2014-10-18 tuned signature;
2014-10-16 wenzelm 2014-10-16 more explicit Line_Nesting;
2014-10-16 wenzelm 2014-10-16 tuned comments;
2014-10-16 wenzelm 2014-10-16 support line context with depth; basic setup for "isabelle" fold handling; misc tuning;
2014-09-30 wenzelm 2014-09-30 tuned;
2014-08-12 wenzelm 2014-08-12 clarified Position.Identified: do not require range from prover, default to command position;
2014-08-12 wenzelm 2014-08-12 maintain Command_Range position as in ML;
2014-08-12 wenzelm 2014-08-12 tuned signature;