src/Pure/PIDE/markup.ML
2 months ago wenzelm 2019-03-24 clarified spell-checking (see also 30233285270a);
2 months ago wenzelm 2019-03-24 more markup for various text kinds, notably for nested formal comments;
2 months ago wenzelm 2019-03-24 documentation of document markers and re-interpreted command tags;
2 months ago wenzelm 2019-03-17 more meta data from "dcterms" (superset of "dc");
2 months ago wenzelm 2019-03-10 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
2 months ago wenzelm 2019-03-10 added semantic document markers; emulate old-style tags as "tag" markers, with subtle change of semantics for multiples tags (ever used?); tuned;
3 months ago wenzelm 2019-02-04 added executable flag for exports; clarified signature;
4 months ago wenzelm 2019-01-14 clarified message;
4 months ago wenzelm 2019-01-13 support hyperlink to theory exports;
4 months ago wenzelm 2018-12-31 update theory sources based on PIDE markup;
5 months ago wenzelm 2018-11-30 more general command 'generate_file' for registered file types, notably Haskell; discontinued 'generate_haskell_file', 'export_haskell_file'; eliminated generated sources: compile files in tmp dir;
6 months ago wenzelm 2018-11-25 tuned signature (see also src/Tools/Haskell/Markup.hs);
6 months ago wenzelm 2018-11-21 more comment markup;
6 months ago wenzelm 2018-11-19 unused -- left-over from Proof General;
6 months ago wenzelm 2018-10-30 added GHC.read_source: read Haskell source text with antiquotations; added "cartouche" antiquotation for ML string expressions as Haskell string literals;
8 months ago wenzelm 2018-09-15 more exports;
8 months ago wenzelm 2018-09-02 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
8 months ago wenzelm 2018-09-01 more explicit status for "canceled" command within theory node;
9 months ago wenzelm 2018-08-27 simplified markup;
12 months ago wenzelm 2018-05-29 more node status information;
12 months ago wenzelm 2018-05-27 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
12 months ago wenzelm 2018-05-07 store exports within PIDE command state; Markup.Export.unapply: proper NAME;
12 months ago wenzelm 2018-05-06 tuned signature; clarified modules;
12 months ago wenzelm 2018-05-06 tuned signature;
12 months ago wenzelm 2018-05-05 protocol message for export of theory resources;
16 months ago wenzelm 2018-01-25 more markup: disable spell-checker for raw latex;
16 months ago wenzelm 2018-01-14 allow LaTeX source as formal comment;
16 months ago wenzelm 2018-01-03 HTML output for Markdown elements; clarified HTML operations;
16 months ago wenzelm 2018-01-02 PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
16 months ago wenzelm 2018-01-02 clarified terminology of "markdown_bullet";
17 months ago wenzelm 2017-12-16 added document antiquotation @{session name}; renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
17 months ago wenzelm 2017-12-12 simplified positions -- line is also human-readable in generated .tex file;
17 months ago wenzelm 2017-12-10 more explicit latex errors;
18 months ago wenzelm 2017-11-04 more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
19 months ago wenzelm 2017-10-16 provide theory timing information, similar to command timing but always considered relevant;
21 months ago wenzelm 2017-08-08 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
23 months ago wenzelm 2017-06-12 tuned signature;
23 months ago wenzelm 2017-06-08 more HTML rendering as in Isabelle/jEdit; tuned;
2017-03-18 wenzelm 2017-03-18 more realistic PIDE build session;
2016-12-28 wenzelm 2016-12-28 more uniform treatment of "bad" like other messages (with serial number);
2016-09-05 wenzelm 2016-09-05 clarified modules;
2016-08-12 wenzelm 2016-08-12 active jEdit actions;
2016-07-13 wenzelm 2016-07-13 obsolete;
2016-07-13 wenzelm 2016-07-13 semantic indentation for unstructured proof scripts;
2016-06-22 wenzelm 2016-06-22 report class parameters within instantiation;
2016-06-21 wenzelm 2016-06-21 position information for literal facts; Markup.entry may have empty kind/name;
2016-04-09 wenzelm 2016-04-09 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
2016-04-01 wenzelm 2016-04-01 more markup;
2016-04-01 wenzelm 2016-04-01 explicit property for unbreakable block;
2016-04-01 wenzelm 2016-04-01 unused;
2016-04-01 wenzelm 2016-04-01 clarified treatment of properties; tuned messages;
2016-03-31 wenzelm 2016-03-31 explicit mixfix block properties;
2016-03-30 wenzelm 2016-03-30 more language markup;
2016-03-05 wenzelm 2016-03-05 more PIDE markup;
2016-01-22 wenzelm 2016-01-22 tuned markup, e.g. relevant for Rendering.tooltip;
2015-12-19 wenzelm 2015-12-19 support for blocks with consistent breaks; tuned;
2015-12-17 wenzelm 2015-12-17 support pretty break indent, like underlying ML systems;
2015-11-13 wenzelm 2015-11-13 added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-10 wenzelm 2015-11-10 added document antiquotation @{theory_text}; tuned document;
2015-11-07 wenzelm 2015-11-07 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);