2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-06-18 wenzelm 2011-06-18 inner literal/delimiter corresponds to outer keyword/operator;
2011-04-26 wenzelm 2011-04-26 clarified auxiliary structure Lexicon.Syntax;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-06 wenzelm 2011-04-06 separate structure Term_Position; dismantled remains of structure Type_Ext;
2011-03-22 wenzelm 2011-03-22 update_name_tr: more precise handling of explicit constraints, including positions;
2011-03-22 wenzelm 2011-03-22 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;
2011-03-21 wenzelm 2011-03-21 added Lexicon.encode_position, Lexicon.decode_position;
2010-11-13 wenzelm 2010-11-13 eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-10-30 wenzelm 2010-10-30 support for floating-point tokens in outer syntax (coinciding with inner syntax version);
2010-09-17 wenzelm 2010-09-17 Syntax.read_asts error: report token ranges within message -- no side-effect here;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_) variants;
2010-09-07 wenzelm 2010-09-07 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase; tuned color;
2010-08-18 wenzelm 2010-08-18 uniform Markup.empty/Markup.Empty in ML and Scala;
2010-08-08 wenzelm 2010-08-08 prefer where a proper context is available -- notably for "inner" entities;
2010-03-03 wenzelm 2010-03-03 more systematic mark/unmark operations; tuned;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2009-01-02 wenzelm 2009-01-02 added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;
2008-12-23 wenzelm 2008-12-23 renamed terminal category "float" to "float_token", to avoid name space conflicts with actual "float" types in user theories (only "float_const" is encountered in practice anyway); tuned;
2008-11-29 nipkow 2008-11-29 New lexical item "float".
2008-09-29 wenzelm 2008-09-29 report_token/parse_token: back to context-less version;
2008-09-29 wenzelm 2008-09-29; parse_token/report_token: explicit context;
2008-08-15 wenzelm 2008-08-15 token_kind: add Space, Comment; tokenize: now includes improper tokens, cf. is_proper; added report_token;
2008-08-09 wenzelm 2008-08-09 pos_of_token: Position.T; removed unused display_token; tuned;
2008-08-09 wenzelm 2008-08-09 datatype token: maintain range, tuned representation; added eof, stopper (from simple_parse.ML); str_of_token: no special case for EOF; misc tuning;
2008-08-07 wenzelm 2008-08-07 improved position handling due to SymbolPos.T;
2008-06-10 wenzelm 2008-06-10 removed obsolete read_idents;
2008-01-28 wenzelm 2008-01-28 basic scanners: produce symbol list instead of imploded string; tuned signature;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated, integer);
2007-09-15 wenzelm 2007-09-15 replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
2007-08-13 wenzelm 2007-08-13 Lexicon.tokenize: do not appen EndToken yet;
2007-07-12 wenzelm 2007-07-12 sys_error;
2007-07-11 wenzelm 2007-07-11 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-04-14 wenzelm 2007-04-14 removed redundant string_of_vname (see term.ML);
2007-04-03 wenzelm 2007-04-03 avoid overloaded integer constants (accomodate Alice);
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-12 wenzelm 2006-12-12 read_xnum: return leading_zeros, radix;
2006-12-11 wenzelm 2006-12-11 xstr: disallow backslashes;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-08-02 wenzelm 2006-08-02 renamed Syntax.indexname to Syntax.read_indexname; added read_int (not Int.fromString, which admits ~ syntax of ML);
2006-07-19 wenzelm 2006-07-19 export is_tid;
2006-07-11 wenzelm 2006-07-11 uniform treatment of num/xnum; read_xnum: proper handling of bin/hex;
2006-07-11 wenzelm 2006-07-11 tuned;
2006-07-11 kleing 2006-07-11 hex and binary numerals (contributed by Rafal Kolanski)
2006-06-17 wenzelm 2006-06-17 moved internal/skolem to term.ML;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-10 wenzelm 2006-02-10 added fixedN, constN;
2005-12-08 wenzelm 2005-12-08 removed Syntax.deskolem;
2005-11-16 wenzelm 2005-11-16 added deskolem;
2005-05-31 wenzelm 2005-05-31 moved is_ident to General/symbol.ML;
2005-05-17 wenzelm 2005-05-17 added read_variable: optional question mark on input; removed obsolete token_assoc; scan_indexname: improved treatment of \<^isub> and \<^isup>; read_var: more robust against bad input; tuned;
2005-05-16 paulson 2005-05-16 Use of instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-18 berghofe 2005-01-18 indexname function now parses type variables as well; changed input type from string list to string.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-29 wenzelm 2004-05-29 Library.read_int; Output.output;