| 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
|
| Sun, 06 Jan 2019 12:42:26 +0100 |
wenzelm |
support for isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2018 16:56:31 +0100 |
wenzelm |
exclude file name components that are special on Windows;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 21:21:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 21:11:24 +0200 |
wenzelm |
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2018 20:32:39 +0100 |
wenzelm |
more position information;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 11:27:52 +0100 |
wenzelm |
discontinued old form of marginal comments;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:08:06 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 15 Jan 2018 22:46:04 +0100 |
wenzelm |
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
|
file |
diff |
annotate
|
| Sun, 14 Jan 2018 19:45:48 +0100 |
wenzelm |
clarified Token.is_text (cf. Parse.text in ML);
|
file |
diff |
annotate
|
| Mon, 04 Dec 2017 22:56:46 +0100 |
wenzelm |
added action to make antiquoted cartouche;
|
file |
diff |
annotate
|
| Wed, 25 Oct 2017 11:40:58 +0200 |
wenzelm |
disallow blanks, relevant for session_name / theory_name e.g. in build log files;
|
file |
diff |
annotate
|
| Wed, 25 Oct 2017 11:35:48 +0200 |
wenzelm |
uniform system name;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 14:59:57 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2017 20:43:26 +0100 |
wenzelm |
support to encode/decode command state;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2017 20:01:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2016 21:00:43 +0100 |
wenzelm |
more precise markup;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2016 13:21:08 +0100 |
wenzelm |
clarified header text;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2016 19:09:10 +0100 |
wenzelm |
more uniform path syntax, as in ML (see 5a7c919a4ada);
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 19:04:49 +0200 |
wenzelm |
clarified indentation: 'begin' is treated like a separate command without indent;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 20:37:28 +0200 |
wenzelm |
indentation of brackets;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 18:18:24 +0200 |
wenzelm |
tunes signature;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 16:36:29 +0200 |
wenzelm |
explicit kind "before_command";
|
file |
diff |
annotate
|
| Thu, 07 Jul 2016 21:34:56 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 17:17:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 12:09:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Sat, 18 Apr 2015 23:43:30 +0200 |
wenzelm |
clarified keywords for quasi-command spans and Sidekick structure;
|
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
|
| Tue, 17 Mar 2015 15:21:41 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 13:32:31 +0100 |
wenzelm |
avoid duplicate header errors, more precise positions;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 21:57:10 +0100 |
wenzelm |
proper command id for inlined errors, which is important for Command.State.accumulate;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 20:35:47 +0100 |
wenzelm |
clarified span position;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 14:46:01 +0100 |
wenzelm |
more command categories, as in ML;
|
file |
diff |
annotate
|
| Sat, 14 Mar 2015 20:08:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 14 Mar 2015 19:51:36 +0100 |
wenzelm |
clarified positions of theory imports;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 20:12:30 +0100 |
wenzelm |
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
|
file |
diff |
annotate
|
| Tue, 09 Dec 2014 21:14:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 14:04:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 11:37:51 +0100 |
wenzelm |
clarified token kind;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 16:57:12 +0100 |
wenzelm |
explicit type Keyword.Keywords;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 15:32:11 +0100 |
wenzelm |
clarified minor/major lexicon (like ML version);
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 15:01:41 +0100 |
wenzelm |
command-line terminator ";" is no longer accepted;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 20:44:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 20:18:37 +0200 |
wenzelm |
proper token kind;
|
file |
diff |
annotate
|
| Tue, 20 May 2014 14:25:28 +0200 |
wenzelm |
explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
|
file |
diff |
annotate
|
| Mon, 19 May 2014 14:48:50 +0200 |
wenzelm |
clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 09:36:38 +0200 |
wenzelm |
tuned message, to accommodate extra brackets produced by Scala parsers;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 13:24:08 +0200 |
wenzelm |
more precise token positions;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 15:38:08 +0100 |
wenzelm |
support ML antiquotations in Scala;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 13:18:08 +0100 |
wenzelm |
tuned signature -- emphasize line-oriented aspect;
|
file |
diff |
annotate
|
| Sat, 15 Feb 2014 18:28:18 +0100 |
wenzelm |
more uniform ML keyword markup;
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 21:06:20 +0100 |
wenzelm |
lexical syntax for SML (in Scala);
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 16:25:30 +0100 |
wenzelm |
tuned signature (in accordance to ML version);
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 15:42:27 +0100 |
wenzelm |
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 16:46:39 +0100 |
wenzelm |
semicolon is minor keyword (see also 29f1e53f9937);
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:31:32 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|