Mon, 25 Feb 2013 13:29:19 +0100 |
wenzelm |
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
|
file |
diff |
annotate
|
Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
Wed, 22 Aug 2012 11:56:13 +0200 |
wenzelm |
tuned errors;
|
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
|
Fri, 16 Mar 2012 21:20:23 +0100 |
wenzelm |
more abstract heading level;
|
file |
diff |
annotate
|
Fri, 16 Mar 2012 20:45:47 +0100 |
wenzelm |
less redundant data;
|
file |
diff |
annotate
|
Fri, 16 Mar 2012 20:33:33 +0100 |
wenzelm |
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
|
file |
diff |
annotate
|
Thu, 15 Mar 2012 00:10:45 +0100 |
wenzelm |
some support for outer syntax keyword declarations within theory header;
|
file |
diff |
annotate
|
Sun, 04 Mar 2012 16:02:14 +0100 |
wenzelm |
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 |
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
|