src/Pure/Syntax/syntax.ML
Fri, 17 Sep 2010 20:42:26 +0200 wenzelm simplified some internal flags using Config.T instead of full-blown Proof_Data;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Tue, 07 Sep 2010 14:08:21 +0200 wenzelm report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
Mon, 06 Sep 2010 21:33:19 +0200 wenzelm more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
Sun, 05 Sep 2010 23:16:21 +0200 wenzelm turned show_brackets into proper configuration option;
Sun, 05 Sep 2010 22:23:48 +0200 wenzelm Syntax.standard_parse_term: eliminated redundant Pretty.pp;
Sun, 05 Sep 2010 22:15:50 +0200 wenzelm structure Syntax: define "interfaces" before actual implementations;
Fri, 03 Sep 2010 22:36:16 +0200 wenzelm configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
Fri, 27 Aug 2010 19:43:28 +0200 wenzelm more careful treatment of context visibility flag wrt. spurious warnings;
Sun, 08 Aug 2010 20:03:31 +0200 wenzelm proper context for Syntax.parse_token;
Sun, 08 Aug 2010 19:54:54 +0200 wenzelm prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
Sat, 07 Aug 2010 21:22:39 +0200 wenzelm more robust treatment of Markup.token;
Sat, 07 Aug 2010 21:03:06 +0200 wenzelm simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
Fri, 02 Jul 2010 21:48:54 +0200 wenzelm standard argument order;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
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;
Sat, 08 May 2010 14:41:23 +0200 wenzelm back-patching via Single_Assignment.var;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Mon, 19 Apr 2010 23:11:39 +0200 wenzelm update_syntax: add new productions only once, to allow repeated local notation, for example;
Tue, 09 Mar 2010 14:29:47 +0100 wenzelm simplified Syntax.basic_syntax (again);
Wed, 03 Mar 2010 00:28:22 +0100 wenzelm authentic syntax for classes and type constructors;
Mon, 01 Mar 2010 17:07:36 +0100 wenzelm more uniform treatment of syntax for types vs. consts;
Sat, 27 Feb 2010 13:32:05 +0100 wenzelm parallel brute-force disambiguation;
Sun, 21 Feb 2010 23:05:37 +0100 wenzelm filter out authentic const syntax;
Mon, 15 Feb 2010 18:03:42 +0100 wenzelm renamed InfixName to Infix etc.;
Thu, 11 Feb 2010 22:03:37 +0100 wenzelm added ML antiquotation @{syntax_const};
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 29 Nov 2009 17:14:24 +0100 wenzelm tuned message;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 18 Mar 2009 21:55:38 +0100 wenzelm de-camelized Symbol_Pos;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Sun, 01 Mar 2009 16:48:06 +0100 wenzelm discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
Wed, 17 Dec 2008 12:10:39 +0100 haftmann dropped Ids
Fri, 05 Dec 2008 18:42:37 +0100 haftmann removed Table.extend, NameSpace.extend_table
Sat, 29 Nov 2008 13:37:13 +0100 nipkow New lexical item "float".
Tue, 18 Nov 2008 18:25:45 +0100 wenzelm tuned;
Mon, 29 Sep 2008 21:26:41 +0200 wenzelm report_token/parse_token: back to context-less version;
Mon, 29 Sep 2008 14:41:25 +0200 wenzelm ContextPosition.report;
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Fri, 15 Aug 2008 15:51:04 +0200 wenzelm read_asts: Lexicon.report_token, filter Lexicon.is_proper;
Sun, 10 Aug 2008 12:38:26 +0200 wenzelm added parse_token (from proof_context.ML);
Sat, 09 Aug 2008 12:28:13 +0200 wenzelm read_asts: report literal tokens;
Sat, 09 Aug 2008 00:09:39 +0200 wenzelm read_token: more robust handling of empty text;
Thu, 07 Aug 2008 22:32:03 +0200 wenzelm added read_token -- with optional YXML encoding of position;
Thu, 07 Aug 2008 13:45:03 +0200 wenzelm adapted Scan.extend_lexicon/merge_lexicons;
Wed, 18 Jun 2008 22:32:04 +0200 wenzelm TypeExt.type_constraint;
Fri, 13 Jun 2008 21:04:42 +0200 wenzelm map_const: soft version, no failure here;
Sun, 18 May 2008 15:04:46 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Thu, 17 Apr 2008 16:30:50 +0200 wenzelm token translations: context dependent, result Pretty.T;
Wed, 16 Apr 2008 17:40:40 +0200 wenzelm tuned;
Wed, 16 Apr 2008 10:50:37 +0200 haftmann educated guess for infix syntax
Sun, 27 Jan 2008 22:21:35 +0100 wenzelm added ambiguity_limit (restricts parse trees / terms printed in messages);
Tue, 27 Nov 2007 16:48:38 +0100 wenzelm standard_parse_term: check ambiguous results without changing the result yet;
Sun, 11 Nov 2007 14:00:13 +0100 wenzelm syntax operations: turned extend'' into update'' (absorb duplicates);
Sat, 10 Nov 2007 23:04:03 +0100 wenzelm added update_const_gram (avoids duplicates);
Sat, 20 Oct 2007 18:54:35 +0200 wenzelm moved internalM to PrintMode.internal;
less more (0) -100 -60 tip