| Tue, 27 Jul 2010 22:15:51 +0200 |
wenzelm |
simplified Thy_Header.read -- include Source.of_string_limited here;
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 14:44:33 +0200 |
wenzelm |
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 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
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 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 21:00:28 +0200 |
wenzelm |
added keyword category "schematic goal", which prevents any attempt to fork the proof;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
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 |
wenzelm |
modernized Thy_Header;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 16:21:47 +0100 |
wenzelm |
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 00:33:13 +0200 |
wenzelm |
present_token: disable print_mode, which is YXML now;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2008 21:28:01 +0200 |
wenzelm |
adapted ThyEdit operations;
|
file |
diff |
annotate
|
| Sun, 20 Jul 2008 23:07:01 +0200 |
wenzelm |
adapted ThyEdit.span;
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:32 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 11:39:29 +0200 |
aspinall |
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 |
wenzelm |
adapted ThyHeader.read;
|
file |
diff |
annotate
|
| Thu, 12 Jul 2007 00:15:35 +0200 |
wenzelm |
Parsing theory sources without execution (via keyword classification).
|
file |
diff |
annotate
|