src/Pure/PIDE/markup.ML
Sun, 13 Nov 2022 20:28:39 +0100 wenzelm ML support for the Prism.js syntax highlighter -- via Isabelle/Scala;
Mon, 31 Oct 2022 11:04:54 +0100 wenzelm clarified signature;
Sat, 29 Oct 2022 21:36:33 +0200 wenzelm tuned signature;
Fri, 26 Aug 2022 12:38:00 +0200 wenzelm removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
Tue, 23 Nov 2021 21:02:13 +0100 wenzelm example: alternative document headings, based on more general document output markup;
Sat, 20 Nov 2021 20:42:41 +0100 wenzelm more symbolic latex_output via XML (using YXML within text);
Sat, 20 Nov 2021 18:15:09 +0100 wenzelm more symbolic latex_output via XML;
Mon, 15 Nov 2021 17:26:31 +0100 wenzelm more symbolic latex_output via XML;
Sun, 14 Nov 2021 20:40:41 +0100 wenzelm more symbolic latex output;
Sun, 14 Nov 2021 17:46:41 +0100 wenzelm symbolic latex_output via XML, interpreted in Isabelle/Scala;
Wed, 03 Nov 2021 16:23:20 +0100 wenzelm more PIDE markup;
Wed, 03 Nov 2021 14:26:13 +0100 wenzelm more PIDE markup;
Tue, 07 Sep 2021 22:35:44 +0200 wenzelm more markup, e.g. to locate defining theory node in formal document output;
Tue, 07 Sep 2021 21:16:22 +0200 wenzelm export other entities, e.g. relevant for formal document output;
Tue, 24 Aug 2021 13:39:37 +0200 wenzelm minor performance tuning;
Tue, 03 Aug 2021 13:08:23 +0200 wenzelm more uniform signatures in ML and Scala;
Tue, 08 Jun 2021 13:17:45 +0200 wenzelm more formal ML profiling messages;
Tue, 25 May 2021 22:28:39 +0200 wenzelm compose Latex text as XML, output exported YXML in Isabelle/Scala;
Sat, 13 Mar 2021 12:36:24 +0100 wenzelm clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
Wed, 09 Dec 2020 22:07:14 +0100 wenzelm clarified protocol: support "isabelle log" on failed theories as well;
Mon, 07 Dec 2020 16:28:44 +0100 wenzelm clarified markup (refining 1c59b555ac4a);
Mon, 07 Dec 2020 16:09:06 +0100 wenzelm more accurate markup (refining 1c59b555ac4a);
Sat, 28 Nov 2020 21:56:24 +0100 wenzelm added document antiquotation @{tool};
Wed, 25 Nov 2020 15:24:55 +0100 wenzelm tuned signature;
Wed, 25 Nov 2020 15:12:02 +0100 wenzelm clarified signature;
Mon, 23 Nov 2020 15:14:58 +0100 wenzelm support for PIDE markup in batch build (inactive due to pide_reports=false);
Tue, 29 Sep 2020 13:19:34 +0200 wenzelm allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
Sat, 15 Aug 2020 13:37:34 +0200 wenzelm provide protocol handlers via isabelle_system_service;
Fri, 07 Aug 2020 22:57:14 +0200 wenzelm provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
Fri, 07 Aug 2020 22:19:32 +0200 wenzelm clarified names;
Fri, 07 Aug 2020 20:19:49 +0200 wenzelm ML statistics via external process: allows monitoring RTS while ML program sleeps;
Thu, 06 Aug 2020 23:13:24 +0200 wenzelm unused;
Thu, 06 Aug 2020 22:43:40 +0200 wenzelm discontinued old batch-build functionality;
Wed, 08 Jul 2020 14:43:02 +0200 wenzelm more robust protocol for "Timing ..." messages, notably for pide_session=true;
Wed, 27 May 2020 20:51:25 +0200 wenzelm clarified markup;
Wed, 27 May 2020 14:27:22 +0200 wenzelm check bash functions against Isabelle settings environment;
Sun, 24 May 2020 19:45:42 +0200 wenzelm proper check of registered Scala functions;
Wed, 02 Oct 2019 14:45:37 +0200 wenzelm more robust: avoid update/interrupt of long-running print_consolidation;
Fri, 06 Sep 2019 19:44:54 +0200 wenzelm prefer commands_accepted: fewer protocol messages;
Sat, 10 Aug 2019 12:53:35 +0200 wenzelm allow duplicate exports via strict = false;
Thu, 02 May 2019 14:05:59 +0200 wenzelm clarified PIDE markup;
Fri, 12 Apr 2019 19:48:29 +0200 wenzelm report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
Sat, 30 Mar 2019 22:51:38 +0100 wenzelm more PIDE markup and hyperlinks;
Sun, 24 Mar 2019 17:53:46 +0100 wenzelm clarified spell-checking (see also 30233285270a);
Sun, 24 Mar 2019 17:24:24 +0100 wenzelm more markup for various text kinds, notably for nested formal comments;
Sun, 24 Mar 2019 13:48:46 +0100 wenzelm documentation of document markers and re-interpreted command tags;
Sun, 17 Mar 2019 20:03:55 +0100 wenzelm more meta data from "dcterms" (superset of "dc");
Sun, 10 Mar 2019 14:19:30 +0100 wenzelm markup and document markers for some meta data from "Dublin Core Metadata Element Set";
Sun, 10 Mar 2019 00:21:34 +0100 wenzelm added semantic document markers;
Mon, 04 Feb 2019 15:45:40 +0100 wenzelm added executable flag for exports;
Mon, 14 Jan 2019 13:58:12 +0100 wenzelm clarified message;
Sun, 13 Jan 2019 19:42:06 +0100 wenzelm support hyperlink to theory exports;
Mon, 31 Dec 2018 13:07:24 +0100 wenzelm update theory sources based on PIDE markup;
Fri, 30 Nov 2018 23:43:10 +0100 wenzelm more general command 'generate_file' for registered file types, notably Haskell;
Sun, 25 Nov 2018 21:10:55 +0100 wenzelm tuned signature (see also src/Tools/Haskell/Markup.hs);
Wed, 21 Nov 2018 14:33:30 +0100 wenzelm more comment markup;
Mon, 19 Nov 2018 12:39:39 +0100 wenzelm unused -- left-over from Proof General;
Tue, 30 Oct 2018 22:05:30 +0100 wenzelm added GHC.read_source: read Haskell source text with antiquotations;
Sat, 15 Sep 2018 23:35:46 +0200 wenzelm more exports;
Sun, 02 Sep 2018 22:30:08 +0200 wenzelm clarified quasi_consolidated state: ensure that exports are present for ok nodes;
less more (0) -100 -60 tip