| Fri, 31 Oct 2014 21:48:40 +0100 |
wenzelm |
discontinued obsolete control command category;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 20:44:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 15:21:44 +0200 |
wenzelm |
support for structure matching;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 13:56:42 +0200 |
wenzelm |
tuned rendering;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 10:53:24 +0200 |
wenzelm |
clarified tree root;
|
file |
diff |
annotate
|
| Sun, 19 Oct 2014 11:20:03 +0200 |
wenzelm |
tuned signature and modules;
|
file |
diff |
annotate
|
| Sat, 18 Oct 2014 22:41:36 +0200 |
wenzelm |
more folds;
|
file |
diff |
annotate
|
| Sat, 18 Oct 2014 20:56:16 +0200 |
wenzelm |
clarified Line_Structure wrt. command span;
|
file |
diff |
annotate
|
| Sat, 18 Oct 2014 10:32:19 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 21:24:42 +0200 |
wenzelm |
more explicit Line_Nesting;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 12:24:19 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 12:09:57 +0200 |
wenzelm |
support line context with depth;
|
file |
diff |
annotate
|
| Tue, 30 Sep 2014 19:37:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:31:24 +0200 |
wenzelm |
clarified Position.Identified: do not require range from prover, default to command position;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 14:15:58 +0200 |
wenzelm |
maintain Command_Range position as in ML;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:23:30 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:17:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:08:32 +0200 |
wenzelm |
separate module Command_Span: mostly syntactic representation;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 22:29:48 +0200 |
wenzelm |
more explicit type Span in Scala, according to ML version;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 20:53:35 +0200 |
wenzelm |
more abstract Prover.Syntax, as proposed by Carst Tankink;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2014 09:34:51 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 20:57:57 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 22 Feb 2014 15:07:33 +0100 |
wenzelm |
refined language context: antiquotes;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 13:23:49 +0100 |
wenzelm |
default completion context via outer syntax;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 13:18:08 +0100 |
wenzelm |
tuned signature -- emphasize line-oriented aspect;
|
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
|
| Mon, 18 Nov 2013 23:26:15 +0100 |
wenzelm |
inline blobs into command, via SHA1 digest;
|
file |
diff |
annotate
|
| Sun, 17 Nov 2013 17:22:55 +0100 |
wenzelm |
explicit indication of thy_load commands;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 15:48:37 +0200 |
wenzelm |
explicit indication of outer syntax with no tokens;
|
file |
diff |
annotate
|
| Mon, 24 Jun 2013 23:33:14 +0200 |
wenzelm |
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
|
file |
diff |
annotate
|
| Sat, 18 May 2013 13:00:05 +0200 |
wenzelm |
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 20:39:09 +0100 |
wenzelm |
adhoc recovery from spurious NPEs, similar quantum-effect behind 7c8ce63a3c00;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 22:34:17 +0100 |
wenzelm |
alternative completion for outer syntax keywords;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 18:04:30 +0200 |
wenzelm |
find files via load commands within theory text;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 16:56:18 +0200 |
wenzelm |
more direct cumulation of (sparse) keywords;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 14:54:29 +0200 |
wenzelm |
some support for thy_load_commands;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 12:15:25 +0200 |
wenzelm |
clarified initialization of Thy_Load, Thy_Info, Session;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2012 14:09:09 +0200 |
wenzelm |
added keyword kind "thy_load" (with optional list of file extensions);
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 15:19:08 +0200 |
wenzelm |
permissive outer syntax wrt. symbol recoding;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 15:01:48 +0200 |
wenzelm |
simplified Document.Node.Header -- internalized errors;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 13:21:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Aug 2012 16:56:42 +0200 |
wenzelm |
refined outer syntax;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 13:55:51 +0200 |
wenzelm |
static outer syntax based on session specifications;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2012 17:26:08 +0200 |
wenzelm |
keyword ";" is declared via prover (as "minor", not "diag");
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 21:20:23 +0100 |
wenzelm |
more abstract heading level;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 11:37:56 +0100 |
wenzelm |
maintain Version.syntax within document state;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 10:16:21 +0100 |
wenzelm |
explicit Outer_Syntax.Decl;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 17:13:25 +0100 |
wenzelm |
prefer final ADTs -- prevent ooddities;
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 20:24:05 +0100 |
wenzelm |
streamlined abstract datatype;
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 19:58:49 +0100 |
wenzelm |
streamlined abstract datatype;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 13:19:19 +0200 |
wenzelm |
avoid pointless completion of illegal control commands;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2011 14:54:29 +0200 |
wenzelm |
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
|
file |
diff |
annotate
|
| Thu, 07 Jul 2011 13:48:30 +0200 |
wenzelm |
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
|
file |
diff |
annotate
|
| Sun, 19 Jun 2011 14:11:06 +0200 |
wenzelm |
some unicode chars for special control symbols;
|
file |
diff |
annotate
|
| Sat, 18 Jun 2011 18:17:08 +0200 |
wenzelm |
hardwired abbreviations for standard control symbols;
|
file |
diff |
annotate
|
| Thu, 16 Jun 2011 17:25:16 +0200 |
wenzelm |
some support for partial scans with explicit context;
|
file |
diff |
annotate
|
| Sat, 13 Nov 2010 22:33:07 +0100 |
wenzelm |
somewhat adhoc replacement for 'thus' and 'hence';
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 15:47:56 +0100 |
wenzelm |
eliminated obsolete heading category -- superseded by heading_level;
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 15:43:06 +0100 |
wenzelm |
treat main theory commands like headings, and nest anything else inside;
|
file |
diff |
annotate
|