src/Pure/Isar/args.ML
Tue, 18 Mar 2014 11:13:38 +0100 wenzelm unused;
Wed, 12 Mar 2014 16:11:47 +0100 wenzelm more explicit markup for Token.Literal;
Mon, 10 Mar 2014 22:14:53 +0100 wenzelm tuned messages -- in accordance to Isabelle/Scala;
Mon, 10 Mar 2014 22:08:51 +0100 wenzelm tuned;
Mon, 10 Mar 2014 21:40:39 +0100 wenzelm proper Args.syntax for slightly odd bundle trickery;
Mon, 10 Mar 2014 20:27:08 +0100 wenzelm more markup;
Mon, 10 Mar 2014 18:06:23 +0100 wenzelm clarified Args.check_src: retain name space information for error output;
Mon, 10 Mar 2014 16:30:07 +0100 wenzelm clarified Args.src: more abstract type, position refers to name only;
Mon, 10 Mar 2014 15:30:29 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 15:20:41 +0100 wenzelm prefer Name_Space.pretty with its builtin markup;
Sun, 09 Mar 2014 16:37:56 +0100 wenzelm tuned signature;
Sat, 08 Mar 2014 21:08:10 +0100 wenzelm modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
Thu, 06 Mar 2014 16:12:26 +0100 wenzelm reject internal term names outright, and complete consts instead;
Thu, 06 Mar 2014 14:38:54 +0100 wenzelm eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
Thu, 06 Mar 2014 13:44:01 +0100 wenzelm more uniform check_const/read_const;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
Wed, 05 Mar 2014 14:19:54 +0100 wenzelm suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
Wed, 05 Mar 2014 13:11:08 +0100 wenzelm clarified init_assignable: make double-sure that initial values are reset;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Tue, 25 Feb 2014 17:23:20 +0100 wenzelm tuned message -- more markup;
Mon, 24 Feb 2014 10:17:29 +0100 wenzelm tuned signature;
Sun, 23 Feb 2014 21:53:01 +0100 wenzelm tuned message;
Mon, 27 Jan 2014 12:10:00 +0100 wenzelm tuned signature;
Wed, 22 Jan 2014 16:03:11 +0100 wenzelm tuned signature;
Sun, 19 Jan 2014 20:52:57 +0100 wenzelm cartouche within nested args (attributes, methods, etc.);
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Fri, 23 Aug 2013 17:01:12 +0200 wenzelm tuned signature;
Tue, 20 Aug 2013 23:20:30 +0200 wenzelm more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;
Tue, 20 Aug 2013 21:17:39 +0200 wenzelm proper exhaustive match (cf. e9beabf045ab);
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Fri, 28 Oct 2011 17:15:52 +0200 wenzelm tuned signature -- refined terminology;
Sun, 21 Aug 2011 20:42:26 +0200 wenzelm tuned Parse.group: delayed failure message;
Sat, 23 Apr 2011 13:53:09 +0200 wenzelm proper binding/report of defined simprocs;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 30 Oct 2010 16:33:58 +0200 wenzelm support for real valued configuration options;
Mon, 17 May 2010 15:11:25 +0200 wenzelm renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Thu, 29 Apr 2010 16:55:22 +0200 wenzelm ProofContext.read_const: allow for type constraint (for fixed variable);
Sat, 13 Mar 2010 20:44:12 +0100 wenzelm removed unused Args.maxidx_values and Element.generalize_facts;
Sat, 06 Mar 2010 15:39:16 +0100 wenzelm eliminated Args.bang_facts (legacy feature);
Sat, 27 Feb 2010 20:51:51 +0100 wenzelm clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
Thu, 25 Feb 2010 22:06:43 +0100 wenzelm clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
Sat, 06 Feb 2010 20:57:07 +0100 wenzelm fixed spelling;
Tue, 10 Nov 2009 14:38:39 +0100 wenzelm bang_facts: legacy feature;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Wed, 18 Mar 2009 21:55:38 +0100 wenzelm de-camelized Symbol_Pos;
Fri, 13 Mar 2009 23:32:40 +0100 wenzelm simplified goal_spec: default to first goal;
Fri, 13 Mar 2009 21:25:15 +0100 wenzelm eliminated type Args.T;
Thu, 12 Mar 2009 15:54:58 +0100 wenzelm Assumption.all_prems_of, Assumption.all_assms_of;
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Mon, 01 Dec 2008 19:41:16 +0100 haftmann new Binding module
Tue, 02 Sep 2008 14:10:28 +0200 wenzelm added binding;
Fri, 15 Aug 2008 15:50:44 +0200 wenzelm Args.name_source(_position) for proper position information;
Sun, 10 Aug 2008 12:38:23 +0200 wenzelm pass token source to typ/term etc.;
Sat, 09 Aug 2008 22:43:53 +0200 wenzelm unified Args.T with OuterLex.token;
Mon, 04 Aug 2008 21:24:17 +0200 wenzelm abstract type Scan.stopper;
less more (0) -100 -60 tip