src/Pure/Thy/thy_header.ML
Mon, 06 Dec 2021 15:34:54 +0100 wenzelm discontinued old-style {* verbatim *} tokens;
Wed, 03 Nov 2021 14:26:13 +0100 wenzelm more PIDE markup;
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots;
Sat, 28 Nov 2020 23:28:56 +0100 wenzelm clarified parsing vs. semantic errors;
Fri, 27 Nov 2020 21:59:23 +0100 wenzelm clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
Fri, 12 Apr 2019 17:09:21 +0200 wenzelm support "tag" marker with scope;
Sun, 10 Mar 2019 21:12:29 +0100 wenzelm document markers are formal comments, and may thus occur anywhere in the command-span;
Sun, 10 Mar 2019 00:21:34 +0100 wenzelm added semantic document markers;
Fri, 08 Mar 2019 17:05:23 +0100 wenzelm clarified modules;
Wed, 28 Nov 2018 16:14:31 +0100 wenzelm clarified signature;
Tue, 27 Nov 2018 21:07:39 +0100 wenzelm more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
Sun, 25 Feb 2018 19:16:32 +0100 wenzelm allow multiple entries of and_list (on both sides);
Wed, 24 Jan 2018 19:50:00 +0100 wenzelm tuned: prefer list operations over Source.source;
Fri, 08 Dec 2017 17:57:29 +0100 wenzelm clarified error;
Tue, 05 Dec 2017 15:55:14 +0100 wenzelm explicit tag for document commands: avoid implicit use of document_tags;
Tue, 05 Dec 2017 14:03:10 +0100 wenzelm tuned signature;
Sun, 05 Nov 2017 17:45:17 +0100 wenzelm more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
Fri, 06 Oct 2017 21:14:00 +0200 wenzelm clarified error for bad session-qualified imports;
Thu, 01 Jun 2017 21:43:36 +0200 wenzelm tuned signature;
Mon, 10 Apr 2017 11:29:47 +0200 wenzelm clarified signature;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Thu, 22 Sep 2016 11:25:27 +0200 wenzelm discontinued raw symbols;
Tue, 02 Aug 2016 17:35:18 +0200 wenzelm support 'abbrevs' within theory header;
Mon, 11 Jul 2016 19:03:08 +0200 wenzelm clarified keywords;
Mon, 11 Jul 2016 18:39:30 +0200 wenzelm clarified keywords;
Sun, 10 Jul 2016 11:18:35 +0200 wenzelm tuned signature: more uniform Keyword.spec;
Tue, 19 Apr 2016 12:06:34 +0200 wenzelm more IDE support for Isabelle/Pure bootstrap;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Sat, 09 Apr 2016 19:30:15 +0200 wenzelm support ROOT0.ML as well -- independently of ROOT.ML;
Wed, 06 Apr 2016 23:45:19 +0200 wenzelm treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
Mon, 04 Apr 2016 17:25:53 +0200 wenzelm clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
Sun, 28 Feb 2016 17:37:20 +0100 wenzelm discontinued old 'header';
Sat, 17 Oct 2015 21:15:10 +0200 wenzelm added 'paragraph', 'subparagraph';
Mon, 17 Aug 2015 19:34:15 +0200 wenzelm support for ML files with/without debugger information;
Mon, 06 Apr 2015 16:00:19 +0200 wenzelm more position information and PIDE markup for command keywords;
Tue, 17 Mar 2015 15:21:41 +0100 wenzelm misc tuning and simplification;
Sat, 14 Mar 2015 18:18:40 +0100 wenzelm misc tuning -- more uniform ML vs. Scala;
Sat, 14 Mar 2015 17:23:58 +0100 wenzelm tunes signature -- more uniform ML vs. Scala;
Thu, 13 Nov 2014 23:45:15 +0100 wenzelm uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
Fri, 07 Nov 2014 17:43:50 +0100 wenzelm tuned;
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Thu, 06 Nov 2014 16:10:33 +0100 wenzelm tuned signature;
Thu, 06 Nov 2014 13:44:14 +0100 wenzelm tuned signature;
Thu, 06 Nov 2014 11:44:41 +0100 wenzelm simplified keyword kinds;
Wed, 05 Nov 2014 22:17:05 +0100 wenzelm tuned signature;
Wed, 05 Nov 2014 21:59:21 +0100 wenzelm more uniform header_keywords in ML/Scala;
Wed, 05 Nov 2014 20:49:30 +0100 wenzelm eliminated pointless dynamic keywords (TTY legacy);
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Sun, 02 Nov 2014 15:27:37 +0100 wenzelm uniform heading commands work in any context, even in theory header;
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Sat, 01 Nov 2014 18:46:48 +0100 wenzelm simplified -- scanning is never interactive;
Sat, 01 Nov 2014 15:01:41 +0100 wenzelm command-line terminator ";" is no longer accepted;
Wed, 30 Apr 2014 22:34:11 +0200 wenzelm some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
Fri, 27 Sep 2013 21:04:57 +0200 wenzelm more robust parser: 'imports' are mandatory except for bootstrapping Pure;
Fri, 05 Apr 2013 20:54:55 +0200 wenzelm tuned signature -- agree with markup terminology;
Wed, 27 Feb 2013 16:27:44 +0100 wenzelm discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
Wed, 27 Feb 2013 12:45:19 +0100 wenzelm discontinued obsolete 'uses' within theory header;
Mon, 19 Nov 2012 22:34:17 +0100 wenzelm alternative completion for outer syntax keywords;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
less more (0) -60 tip