src/Pure/Tools/rail.ML
2016-04-01 wenzelm 2016-04-01 more markup;
2016-04-01 wenzelm 2016-04-01 tuned signature;
2016-03-29 wenzelm 2016-03-29 tuned signature;
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-10-18 wenzelm 2015-10-18 clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned;
2015-10-17 wenzelm 2015-10-17 clarified Latex.environment;
2015-10-16 wenzelm 2015-10-16 clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;
2015-10-15 wenzelm 2015-10-15 trim_blanks after read, before eval; clarified Raw_Token: uniform output_text; tuned signature;
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;