Fri, 16 Mar 2012 20:45:47 +0100 |
less redundant data;
|
file | diff | annotate |
Fri, 16 Mar 2012 20:33:33 +0100 |
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
|
file | diff | annotate |
Thu, 15 Mar 2012 00:10:45 +0100 |
some support for outer syntax keyword declarations within theory header;
|
file | diff | annotate |
Sun, 04 Mar 2012 16:02:14 +0100 |
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
|
file | diff | annotate |
Tue, 27 Jul 2010 22:15:51 +0200 |
simplified Thy_Header.read -- include Source.of_string_limited here;
|
file | diff | annotate |
Tue, 20 Jul 2010 14:44:33 +0200 |
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
|
file | diff | annotate |
Mon, 31 May 2010 21:06:57 +0200 |
modernized some structure names, keeping a few legacy aliases;
|
file | diff | annotate |
Thu, 27 May 2010 18:10:37 +0200 |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
Sat, 15 May 2010 23:16:32 +0200 |
refer directly to structure Keyword and Parse;
|
file | diff | annotate |
Fri, 23 Apr 2010 21:00:28 +0200 |
added keyword category "schematic goal", which prevents any attempt to fork the proof;
|
file | diff | annotate |
Wed, 21 Oct 2009 08:14:38 +0200 |
dropped redundant gen_ prefix
|
file | diff | annotate |
Tue, 20 Oct 2009 16:13:01 +0200 |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file | diff | annotate |
Tue, 01 Sep 2009 14:45:06 +0200 |
modernized Thy_Header;
|
file | diff | annotate |
Wed, 21 Jan 2009 23:21:44 +0100 |
removed Ids;
|
file | diff | annotate |
Fri, 02 Jan 2009 16:21:47 +0100 |
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
|
file | diff | annotate |
Thu, 28 Aug 2008 00:33:13 +0200 |
present_token: disable print_mode, which is YXML now;
|
file | diff | annotate |
Tue, 12 Aug 2008 21:28:01 +0200 |
adapted ThyEdit operations;
|
file | diff | annotate |
Sun, 20 Jul 2008 23:07:01 +0200 |
adapted ThyEdit.span;
|
file | diff | annotate |
Wed, 25 Jun 2008 17:38:32 +0200 |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file | diff | annotate |
Thu, 09 Aug 2007 11:39:29 +0200 |
PGIP change: thyname is optional in opentheory, markup even in case of header parse failure
|
file | diff | annotate |
Thu, 19 Jul 2007 23:18:55 +0200 |
adapted ThyHeader.read;
|
file | diff | annotate |
Thu, 12 Jul 2007 00:15:35 +0200 |
Parsing theory sources without execution (via keyword classification).
|
file | diff | annotate |