| 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
|
| Wed, 10 Nov 2010 15:17:25 +0100 |
wenzelm |
default Sidekick parser based on section headings;
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 15:00:40 +0100 |
wenzelm |
some support for nested source structure, based on section headings;
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 22:57:11 +0200 |
wenzelm |
report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 14:23:54 +0200 |
wenzelm |
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 22:05:49 +0200 |
wenzelm |
renamed Outer_Keyword to Keyword (in Scala);
|
file |
diff |
annotate
|
| Tue, 05 Jan 2010 15:44:06 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 22 Dec 2009 19:38:06 +0100 |
wenzelm |
renamed class Outer_Keyword to Outer_Syntax;
|
file |
diff |
annotate
|