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