| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
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
|
| Sun, 12 Aug 2012 19:09:55 +0200 |
wenzelm |
more static antiquotations;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 22:17:46 +0200 |
wenzelm |
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 12:36:54 +0200 |
wenzelm |
more official command specifications, including source position;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 12:26:19 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 19:48:19 +0100 |
wenzelm |
added ML antiquotation @{keyword};
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 20:36:18 +0200 |
wenzelm |
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 18:25:50 +0200 |
wenzelm |
clarified Type.the_decl;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 22:40:29 +0200 |
wenzelm |
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Sun, 09 Jan 2011 21:33:41 +0100 |
wenzelm |
reverted 08240feb69c7 -- breaks positions of reports;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 21:05:50 +0100 |
wenzelm |
more robust ML antiquotations -- allow original tokens without adjacent whitespace;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 23:19:52 +0200 |
wenzelm |
discontinued obsolete ML antiquotation @{theory_ref};
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 11:16:23 +0200 |
wenzelm |
added ML antiquotation @{assert};
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 15:02:51 +0200 |
wenzelm |
ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
|
file |
diff |
annotate
|
| Thu, 03 Jun 2010 22:06:37 +0200 |
wenzelm |
allow qualified names;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 10:52:10 +0200 |
wenzelm |
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 14:36:41 +0100 |
wenzelm |
ProofContext.read_class/read_type_name_proper;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:28:22 +0100 |
wenzelm |
authentic syntax for classes and type constructors;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 20:56:03 +0100 |
wenzelm |
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 13:32:38 +0100 |
wenzelm |
ML antiquotations for type classes;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:08:43 +0100 |
wenzelm |
more orthogonal antiquotations for type constructors;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 21:08:25 +0100 |
wenzelm |
authentic syntax for *all* term constants;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 11:27:29 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:03:37 +0100 |
wenzelm |
added ML antiquotation @{syntax_const};
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 18:04:48 +0100 |
wenzelm |
simplified interface for ML antiquotations, struct_name is always "Isabelle";
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:21:11 +0100 |
wenzelm |
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2009 21:35:49 +0100 |
wenzelm |
@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:43 +0100 |
wenzelm |
ML_Syntax.make_binding;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 21:49:05 +0100 |
wenzelm |
added @{binding} ML antiquotations;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2008 15:50:44 +0200 |
wenzelm |
Args.name_source(_position) for proper position information;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:54 +0200 |
wenzelm |
ML_Context.add_antiq: pass position;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 22:52:11 +0200 |
wenzelm |
moved theorem values to ml_thms.ML;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 15:17:28 +0200 |
wenzelm |
added macro interface;
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 15:06:25 +0200 |
wenzelm |
Args.context;
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:39 +0200 |
wenzelm |
re-use official outer keywords;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:16 +0200 |
wenzelm |
Common ML antiquotations.
|
file |
diff |
annotate
|