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
|