Wed, 06 Apr 2011 23:04:00 +0200 |
wenzelm |
separate structure Term_Position;
|
file |
diff |
annotate
|
Wed, 06 Apr 2011 21:55:41 +0200 |
wenzelm |
moved type syntax translations to syn_trans.ML;
|
file |
diff |
annotate
|
Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
Wed, 06 Apr 2011 12:58:13 +0200 |
wenzelm |
moved unparse material to syntax_phases.ML;
|
file |
diff |
annotate
|
Tue, 05 Apr 2011 23:14:41 +0200 |
wenzelm |
moved decode/parse operations to standard_syntax.ML;
|
file |
diff |
annotate
|
Tue, 05 Apr 2011 13:07:40 +0200 |
wenzelm |
more precise propagation of reports/results through some inner syntax layers;
|
file |
diff |
annotate
|
Sun, 03 Apr 2011 21:59:33 +0200 |
wenzelm |
added Position.reports convenience;
|
file |
diff |
annotate
|
Tue, 29 Mar 2011 21:48:01 +0200 |
wenzelm |
use shared copy of hoare_syntax.ML;
|
file |
diff |
annotate
|
Tue, 29 Mar 2011 21:11:02 +0200 |
wenzelm |
Hoare syntax: standard abstraction syntax admits source positions;
|
file |
diff |
annotate
|
Sat, 26 Mar 2011 12:01:40 +0100 |
wenzelm |
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
|
file |
diff |
annotate
|
Sat, 26 Mar 2011 10:52:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 26 Mar 2011 10:25:17 +0100 |
wenzelm |
dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
|
file |
diff |
annotate
|
Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file |
diff |
annotate
|
Thu, 24 Mar 2011 11:45:39 +0100 |
wenzelm |
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
|
file |
diff |
annotate
|
Tue, 22 Mar 2011 20:44:47 +0100 |
wenzelm |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
file |
diff |
annotate
|
Tue, 22 Mar 2011 17:51:15 +0100 |
wenzelm |
binder_tr: more informative exception;
|
file |
diff |
annotate
|
Tue, 22 Mar 2011 16:15:50 +0100 |
wenzelm |
update_name_tr: more precise handling of explicit constraints, including positions;
|
file |
diff |
annotate
|
Tue, 22 Mar 2011 13:32:20 +0100 |
wenzelm |
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
|
file |
diff |
annotate
|
Mon, 21 Mar 2011 21:16:39 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 21 Mar 2011 20:56:44 +0100 |
wenzelm |
clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
|
file |
diff |
annotate
|
Thu, 28 Oct 2010 22:04:00 +0200 |
wenzelm |
use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
|
file |
diff |
annotate
|
Mon, 06 Sep 2010 21:33:19 +0200 |
wenzelm |
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
|
file |
diff |
annotate
|
Fri, 03 Sep 2010 23:54:48 +0200 |
wenzelm |
turned eta_contract into proper configuration option;
|
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, 29 Apr 2010 11:00:32 +0200 |
wenzelm |
uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
|
file |
diff |
annotate
|
Wed, 03 Mar 2010 00:28:22 +0100 |
wenzelm |
authentic syntax for classes and type constructors;
|
file |
diff |
annotate
|
Sun, 21 Feb 2010 21:08:25 +0100 |
wenzelm |
authentic syntax for *all* term constants;
|
file |
diff |
annotate
|
Thu, 18 Feb 2010 11:23:03 +0100 |
wenzelm |
made SML/NJ happy (again);
|
file |
diff |
annotate
|
Tue, 16 Feb 2010 14:08:39 +0100 |
wenzelm |
moved generic update_name to Pure syntax -- not specific to HOL/record;
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:25:50 +0200 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Tue, 21 Jul 2009 14:38:07 +0200 |
haftmann |
attempt for more concise setup of non-etacontracting binders
|
file |
diff |
annotate
|
Wed, 10 Jun 2009 11:12:06 +0200 |
wenzelm |
reraise exceptions to preserve position information;
|
file |
diff |
annotate
|
Fri, 27 Feb 2009 16:38:52 +0100 |
wenzelm |
eliminated NJ's List.nth;
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 19:54:03 +0100 |
wenzelm |
qualified Term.rename_wrt_term;
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
Thu, 16 Oct 2008 22:44:37 +0200 |
wenzelm |
added translations for SORT_CONSTRAINT
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
Tue, 24 Jul 2007 19:44:35 +0200 |
wenzelm |
moved exception capture/release to structure Exn;
|
file |
diff |
annotate
|
Mon, 23 Jul 2007 19:45:44 +0200 |
wenzelm |
eliminated transform_failure (to avoid critical section for main transactions);
|
file |
diff |
annotate
|
Tue, 17 Jul 2007 13:19:19 +0200 |
wenzelm |
moved print_translations from Pure.thy to Syntax/syn_trans.ML;
|
file |
diff |
annotate
|
Mon, 11 Dec 2006 21:39:28 +0100 |
wenzelm |
advanced translation functions: Proof.context;
|
file |
diff |
annotate
|
Sun, 10 Dec 2006 15:30:53 +0100 |
wenzelm |
abs/binder_tr': support printing of idtdummy;
|
file |
diff |
annotate
|
Sun, 26 Nov 2006 18:07:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 25 Jul 2006 21:18:09 +0200 |
wenzelm |
added variant_abs (from term.ML);
|
file |
diff |
annotate
|
Tue, 18 Jul 2006 20:01:41 +0200 |
wenzelm |
Term.declare_term_names;
|
file |
diff |
annotate
|
Tue, 11 Jul 2006 12:17:01 +0200 |
wenzelm |
Name.invent_list;
|
file |
diff |
annotate
|
Sun, 11 Jun 2006 21:59:28 +0200 |
wenzelm |
improved treatment of TERM TYPE syntax;
|
file |
diff |
annotate
|
Fri, 05 May 2006 21:59:45 +0200 |
wenzelm |
added syntax for _type_constraint_;
|
file |
diff |
annotate
|
Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 21 Mar 2006 12:18:22 +0100 |
wenzelm |
mark_boundT: produce well-typed term;
|
file |
diff |
annotate
|
Thu, 23 Feb 2006 13:37:46 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
Wed, 22 Feb 2006 22:18:42 +0100 |
wenzelm |
removed obsolete meta_conjunction_tr';
|
file |
diff |
annotate
|
Fri, 10 Feb 2006 02:22:56 +0100 |
wenzelm |
moved fixedN to lexicon.ML;
|
file |
diff |
annotate
|
Mon, 06 Feb 2006 20:59:58 +0100 |
wenzelm |
added bound_vars;
|
file |
diff |
annotate
|
Tue, 31 Jan 2006 00:39:40 +0100 |
wenzelm |
advanced translations: Context.generic;
|
file |
diff |
annotate
|
Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
Thu, 22 Dec 2005 00:29:10 +0100 |
wenzelm |
prop_tr': proper handling of aprop marked as bound;
|
file |
diff |
annotate
|
Fri, 02 Dec 2005 22:54:52 +0100 |
wenzelm |
asts_to_terms: builtin free_fixed translation makes local binders work properly;
|
file |
diff |
annotate
|