Fri, 16 Mar 2012 14:42:11 +0100defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm [Fri, 16 Mar 2012 14:42:11 +0100] rev 47830
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;

Fri, 16 Mar 2012 13:05:30 +0100define keywords early when processing the theory header, before running the body commands;
wenzelm [Fri, 16 Mar 2012 13:05:30 +0100] rev 47829
define keywords early when processing the theory header, before running the body commands;

Fri, 16 Mar 2012 11:26:55 +0100clarified Keyword.is_keyword: union of minor and major;
wenzelm [Fri, 16 Mar 2012 11:26:55 +0100] rev 47828
clarified Keyword.is_keyword: union of minor and major;
misc tuning and simplification;

Thu, 15 Mar 2012 23:06:22 +0100Isabelle/jEdit supports user-defined Isar commands within the running session;
wenzelm [Thu, 15 Mar 2012 23:06:22 +0100] rev 47827
Isabelle/jEdit supports user-defined Isar commands within the running session;

Thu, 15 Mar 2012 22:21:28 +0100merged
wenzelm [Thu, 15 Mar 2012 22:21:28 +0100] rev 47826
merged

Thu, 15 Mar 2012 22:20:07 +0100more precise TPTP keywords and dependencies;
wenzelm [Thu, 15 Mar 2012 22:20:07 +0100] rev 47825
more precise TPTP keywords and dependencies;

Thu, 15 Mar 2012 22:08:53 +0100declare command keywords via theory header, including strict checking outside Pure;
wenzelm [Thu, 15 Mar 2012 22:08:53 +0100] rev 47824
declare command keywords via theory header, including strict checking outside Pure;

Thu, 15 Mar 2012 20:07:00 +0100prefer formally checked @{keyword} parser;
wenzelm [Thu, 15 Mar 2012 20:07:00 +0100] rev 47823
prefer formally checked @{keyword} parser;

Thu, 15 Mar 2012 19:48:19 +0100added ML antiquotation @{keyword};
wenzelm [Thu, 15 Mar 2012 19:48:19 +0100] rev 47822
added ML antiquotation @{keyword};

Thu, 15 Mar 2012 19:02:34 +0100declare minor keywords via theory header;
wenzelm [Thu, 15 Mar 2012 19:02:34 +0100] rev 47821
declare minor keywords via theory header;