Mon, 07 Dec 2020 15:54:07 +0100 |
wenzelm |
tuned signature --- more operations;
|
file |
diff |
annotate
|
Sun, 28 Apr 2019 13:09:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 03 Apr 2019 21:50:00 +0200 |
wenzelm |
clarified signature: more explicit operations for corresponding Isar commands;
|
file |
diff |
annotate
|
Sun, 10 Mar 2019 21:12:29 +0100 |
wenzelm |
document markers are formal comments, and may thus occur anywhere in the command-span;
|
file |
diff |
annotate
|
Fri, 08 Mar 2019 17:05:23 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Thu, 03 Jan 2019 16:42:15 +0100 |
wenzelm |
mixfix annotations may use cartouches;
|
file |
diff |
annotate
|
Thu, 03 Jan 2019 16:13:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Sat, 16 Dec 2017 16:46:01 +0100 |
wenzelm |
PIDE markup for session ROOT files;
|
file |
diff |
annotate
|
Tue, 05 Dec 2017 14:03:10 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 12 Aug 2016 13:16:04 +0200 |
wenzelm |
more uniform path syntax (like url);
|
file |
diff |
annotate
|
Sat, 11 Jun 2016 16:41:11 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
Mon, 06 Jun 2016 08:13:07 +0200 |
wenzelm |
avoid multiple reports on shared type;
|
file |
diff |
annotate
|
Tue, 24 May 2016 16:13:59 +0200 |
wenzelm |
simplified syntax;
|
file |
diff |
annotate
|
Tue, 24 May 2016 15:53:16 +0200 |
wenzelm |
simplified syntax: Parse.term corresponds to Args.term etc.;
|
file |
diff |
annotate
|
Mon, 23 May 2016 21:30:30 +0200 |
wenzelm |
embedded content may be delimited via cartouches;
|
file |
diff |
annotate
|
Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
Wed, 13 Apr 2016 11:31:13 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 22:13:08 +0200 |
wenzelm |
tuned -- more explicit sections;
|
file |
diff |
annotate
|
Wed, 30 Mar 2016 14:59:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 29 Mar 2016 21:17:29 +0200 |
wenzelm |
more position information for type mixfix;
|
file |
diff |
annotate
|
Sun, 06 Mar 2016 16:19:02 +0100 |
wenzelm |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
file |
diff |
annotate
|
Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 17 Oct 2015 22:31:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 02 Jul 2015 12:33:04 +0200 |
wenzelm |
allow to specify suffix of goal parameters;
|
file |
diff |
annotate
|
Thu, 11 Jun 2015 22:47:53 +0200 |
wenzelm |
support for 'consider' command;
|
file |
diff |
annotate
|
Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
Sat, 04 Apr 2015 21:21:40 +0200 |
wenzelm |
more general notion of command span: command keyword not necessarily at start;
|
file |
diff |
annotate
|
Fri, 03 Apr 2015 20:04:16 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
Wed, 25 Mar 2015 11:39:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 23 Mar 2015 16:10:32 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 14 Mar 2015 17:23:58 +0100 |
wenzelm |
tunes signature -- more uniform ML vs. Scala;
|
file |
diff |
annotate
|
Wed, 03 Dec 2014 11:37:51 +0100 |
wenzelm |
clarified token kind;
|
file |
diff |
annotate
|
Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
Sat, 22 Nov 2014 13:38:15 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
Wed, 05 Nov 2014 22:17:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 01 Nov 2014 15:01:41 +0100 |
wenzelm |
command-line terminator ";" is no longer accepted;
|
file |
diff |
annotate
|
Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 17:54:09 +0200 |
wenzelm |
allow text cartouches in regular outer syntax categories "text" and "altstring";
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 12:25:17 +0100 |
wenzelm |
more markup for improper elements;
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 11:27:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 12 Mar 2014 16:11:47 +0100 |
wenzelm |
more explicit markup for Token.Literal;
|
file |
diff |
annotate
|
Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
Wed, 26 Feb 2014 11:14:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 24 Feb 2014 10:17:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 22 Jan 2014 16:03:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
Tue, 14 May 2013 19:48:31 +0200 |
wenzelm |
more uniform Markup.parse_real;
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 12:56:26 +0200 |
wenzelm |
just one syntax category "mixfix" -- check structure annotation semantically;
|
file |
diff |
annotate
|
Fri, 05 Apr 2013 20:54:55 +0200 |
wenzelm |
tuned signature -- agree with markup terminology;
|
file |
diff |
annotate
|
Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
Thu, 23 Aug 2012 17:46:03 +0200 |
wenzelm |
tuned messages: end-of-input rarely means physical end-of-file from the past;
|
file |
diff |
annotate
|
Wed, 22 Aug 2012 12:47:49 +0200 |
wenzelm |
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
|
file |
diff |
annotate
|
Wed, 14 Mar 2012 17:52:38 +0100 |
wenzelm |
source positions for locale and class expressions;
|
file |
diff |
annotate
|