2015-04-06 wenzelm 2015-04-06 clarified rail syntax;
2015-03-25 wenzelm 2015-03-25 tuned signature;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-09-26 wenzelm 2014-09-26 proper range for Antiq tokens; more detailed parse trees; report sub-expressions;
2014-03-15 wenzelm 2014-03-15 tuned markup;
2014-03-15 wenzelm 2014-03-15 more markup;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-19 wenzelm 2014-02-19 more markup; clarified token range;
2014-02-17 wenzelm 2014-02-17 more markup;
2014-01-22 wenzelm 2014-01-22 prefer rail cartouche -- avoid back-slashed quotes; proper documentation of \<newline> syntax;
2014-01-17 wenzelm 2014-01-17 prefer user-space tool within Pure.thy;