src/Doc/antiquote_setup.ML
23 months ago wenzelm 2017-09-21 avoid duplicate message for @{action} in particular (see also @{action} within Pure);
2016-04-03 wenzelm 2016-04-03 clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
2015-12-20 wenzelm 2015-12-20 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-11-10 wenzelm 2015-11-10 more thorough check_action, including completion;
2015-11-10 wenzelm 2015-11-10 tuned signature;
2015-11-10 wenzelm 2015-11-10 more thorough check_command, including completion;
2015-11-10 wenzelm 2015-11-10 clarified modules;
2015-11-10 wenzelm 2015-11-10 unused;
2015-11-10 wenzelm 2015-11-10 ignore pointless/unused options;
2015-10-17 wenzelm 2015-10-17 clarified Latex.environment;
2015-03-25 wenzelm 2015-03-25 tuned signature;
2014-12-22 wenzelm 2014-12-22 system option "pretty_margin" is superseded by "thy_output_margin";
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-12-03 wenzelm 2014-12-03 tuned;
2014-11-30 wenzelm 2014-11-30 tuned signature;
2014-11-30 wenzelm 2014-11-30 tuned signature;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
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 clarified keyword categories; tuned;
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-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
2014-11-06 wenzelm 2014-11-06 prefer explicit Keyword.keywords;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-10-20 wenzelm 2014-10-20 official support for "tt" style variants, avoid fragile \verb in LaTeX; official document antiquotation @{verbatim};
2014-08-28 wenzelm 2014-08-28 more liberal embedded "text", which includes cartouches;
2014-08-12 wenzelm 2014-08-12 tuned signature according to Scala version -- prefer explicit argument;
2014-07-01 wenzelm 2014-07-01 redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
2014-06-16 wenzelm 2014-06-16 formal check of jEdit actions;
2014-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2014-03-27 wenzelm 2014-03-27 redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2014-03-25 wenzelm 2014-03-25 separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-17 wenzelm 2014-03-17 more antiquotations;
2014-03-13 wenzelm 2014-03-13 added ML antiquotation @{path};
2014-03-12 wenzelm 2014-03-12 ML_Context.check_antiquotation still required;
2014-03-12 wenzelm 2014-03-12 tuned;
2014-03-12 wenzelm 2014-03-12 some document antiquotations for Isabelle/jEdit elements; modernized theory setup;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-03-02 wenzelm 2014-03-02 clarified names of antiquotations and markup; more documentation;
2014-03-02 wenzelm 2014-03-02 more markup for ML source;
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-25 wenzelm 2014-02-25 proper context for global data;
2014-02-25 wenzelm 2014-02-25 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion; removed obsolete Method.Source_i; proper context for global data; tuned messages;
2013-12-09 wenzelm 2013-12-09 provide @{file_unchecked} in Isabelle/Pure;
2013-11-07 wenzelm 2013-11-07 misc tuning;
2013-08-18 wenzelm 2013-08-18 more markup;
2013-08-16 wenzelm 2013-08-16 check_tool wrt. official ISABELLE_TOOLS; added Path.split (cf. Scala version);
2013-08-16 wenzelm 2013-08-16 more markup via Name_Space.check; tuned signature;
2013-06-15 wenzelm 2013-06-15 updated operations on proof terms;
2012-11-26 wenzelm 2012-11-26 tuned signature; tuned;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-28 wenzelm 2012-08-28 renamed doc-src to src/Doc; renamed TutorialI to Tutorial;