src/Pure/Syntax/lexicon.ML
Wed, 27 Jan 2021 14:56:40 +0100 wenzelm tuned signature (e.g. see HTML.control_block in Isabelle/Scala);
Tue, 19 Jan 2021 20:23:13 +0100 wenzelm suppress markup for literal tokens with block control symbols, for better PIDE/HTML output (see also d15fe10593ff);
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature;
Sun, 10 Mar 2019 21:12:29 +0100 wenzelm document markers are formal comments, and may thus occur anywhere in the command-span;
Sun, 25 Nov 2018 18:45:10 +0100 wenzelm tuned spelling;
Wed, 21 Nov 2018 14:33:30 +0100 wenzelm more comment markup;
Sun, 23 Sep 2018 19:59:53 +0200 wenzelm discontinued old-style inner comments;
Wed, 31 Jan 2018 14:11:57 +0100 wenzelm tuned;
Wed, 31 Jan 2018 14:02:37 +0100 wenzelm more efficient tokens_match_ord based on token_kind_index;
Wed, 31 Jan 2018 11:49:56 +0100 wenzelm more abstract type;
Wed, 31 Jan 2018 11:40:26 +0100 wenzelm clarified signature;
Wed, 31 Jan 2018 11:26:50 +0100 wenzelm clarified signature;
Wed, 31 Jan 2018 11:23:53 +0100 wenzelm explicit dummy token;
Wed, 31 Jan 2018 11:18:36 +0100 wenzelm clarified modules;
Wed, 31 Jan 2018 11:09:05 +0100 wenzelm clarified signature;
Tue, 30 Jan 2018 18:38:18 +0100 wenzelm tuned data structure and operations;
Tue, 30 Jan 2018 11:48:38 +0100 wenzelm clarified modules;
Sun, 28 Jan 2018 19:28:52 +0100 wenzelm clarified take/drop/chop prefix/suffix;
Mon, 15 Jan 2018 23:03:01 +0100 wenzelm clarified markup;
Sun, 14 Jan 2018 15:06:27 +0100 wenzelm clarified signature;
Sun, 14 Jan 2018 14:11:02 +0100 wenzelm clarified modules: uniform notion of formal comments;
Sat, 13 Jan 2018 11:22:46 +0100 wenzelm added \<^cancel> operator for unused text;
Fri, 12 Jan 2018 20:19:59 +0100 wenzelm tuned;
Tue, 09 Jan 2018 17:09:34 +0100 wenzelm clarified markup: more like outer syntax side-comment;
Sun, 07 Jan 2018 21:28:03 +0100 wenzelm tuned whitespace;
Sun, 07 Jan 2018 15:12:00 +0100 wenzelm clarified modules;
Sat, 06 Jan 2018 16:56:07 +0100 wenzelm inner syntax comments may be written as "\<comment> \<open>text\<close>";
Mon, 17 Oct 2016 15:46:51 +0200 wenzelm accomodate Poly/ML repository version, which treats singleton strings as boxed;
Sat, 02 Apr 2016 21:10:07 +0200 wenzelm careful export of type-dependent functions, without losing their special status;
Thu, 31 Mar 2016 16:23:25 +0200 wenzelm clarified modules;
Tue, 29 Mar 2016 20:53:52 +0200 wenzelm tuned signature;
Fri, 18 Mar 2016 16:26:35 +0100 wenzelm clarified modules;
Sun, 06 Mar 2016 16:19:02 +0100 wenzelm clarified treatment of fragments of Isabelle symbols during bootstrap;
Sun, 18 Oct 2015 21:30:01 +0200 wenzelm tuned signature;
Mon, 29 Dec 2014 15:38:59 +0100 wenzelm more toplevel pretty printing;
Fri, 31 Oct 2014 22:02:49 +0100 wenzelm discontinued obsolete \<^sync> marker;
Mon, 22 Sep 2014 21:28:57 +0200 wenzelm discontinued old "xnum" token category;
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Thu, 06 Mar 2014 21:32:09 +0100 wenzelm special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
Thu, 20 Feb 2014 17:51:16 +0100 wenzelm tuned messages;
Wed, 22 Jan 2014 15:10:33 +0100 wenzelm inner syntax token language allows regular quoted strings;
Mon, 20 Jan 2014 20:38:51 +0100 wenzelm tuned signature;
Mon, 20 Jan 2014 20:24:44 +0100 wenzelm tuned error messages, more accurate position;
Mon, 20 Jan 2014 20:04:52 +0100 wenzelm tuned -- more direct err_prefix;
Sat, 18 Jan 2014 19:31:32 +0100 wenzelm unused;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Thu, 12 Dec 2013 22:56:28 +0100 wenzelm discontinued legacy_isub_isup;
Tue, 13 Aug 2013 17:26:22 +0200 wenzelm disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
Thu, 08 Aug 2013 17:36:14 +0200 wenzelm more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
Wed, 10 Jul 2013 16:25:26 +0200 wenzelm more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
Mon, 27 May 2013 22:25:32 +0200 wenzelm more literal tokens, e.g. "EX!";
Thu, 04 Apr 2013 12:06:23 +0200 wenzelm added var_position in analogy to longid_position, for typing reports on input;
Tue, 27 Nov 2012 19:22:36 +0100 wenzelm support for sub-structured identifier syntax (inactive);
Mon, 26 Nov 2012 21:46:04 +0100 wenzelm tuned signature;
Mon, 26 Nov 2012 21:10:42 +0100 wenzelm more uniform Symbol.is_ascii_identifier in ML/Scala;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Thu, 11 Oct 2012 20:38:02 +0200 wenzelm clarified output token markup (see also bc22daeed49e);
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Wed, 15 Feb 2012 13:24:22 +0100 wenzelm renamed "xstr" to "str_token";
Thu, 01 Dec 2011 12:25:27 +0100 wenzelm renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Tue, 06 Sep 2011 20:37:07 +0200 wenzelm bulk reports for improved message throughput;
Sun, 04 Sep 2011 19:36:19 +0200 wenzelm eliminated markup for plain identifiers (frequent but insignificant);
Sat, 23 Jul 2011 16:37:17 +0200 wenzelm defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
Sat, 18 Jun 2011 12:37:42 +0200 wenzelm inner literal/delimiter corresponds to outer keyword/operator;
Tue, 26 Apr 2011 21:05:52 +0200 wenzelm clarified auxiliary structure Lexicon.Syntax;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Wed, 06 Apr 2011 23:04:00 +0200 wenzelm separate structure Term_Position;
Tue, 22 Mar 2011 16:15:50 +0100 wenzelm update_name_tr: more precise handling of explicit constraints, including positions;
Tue, 22 Mar 2011 13:32:20 +0100 wenzelm support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
Mon, 21 Mar 2011 23:38:32 +0100 wenzelm added Lexicon.encode_position, Lexicon.decode_position;
Sat, 13 Nov 2010 19:47:23 +0100 wenzelm eliminated slightly odd pervasive Symbol_Pos.symbol;
Sat, 30 Oct 2010 15:26:40 +0200 wenzelm support for floating-point tokens in outer syntax (coinciding with inner syntax version);
Fri, 17 Sep 2010 21:04:56 +0200 wenzelm Syntax.read_asts error: report token ranges within message -- no side-effect here;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
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;
Wed, 18 Aug 2010 11:02:47 +0200 wenzelm uniform Markup.empty/Markup.Empty in ML and Scala;
Sun, 08 Aug 2010 19:54:54 +0200 wenzelm prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
Wed, 03 Mar 2010 00:00:44 +0100 wenzelm more systematic mark/unmark operations;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Wed, 18 Mar 2009 21:55:38 +0100 wenzelm de-camelized Symbol_Pos;
Mon, 19 Jan 2009 20:05:41 +0100 wenzelm removed Ids;
Fri, 02 Jan 2009 19:38:13 +0100 wenzelm added numeral, which supercedes num, xnum, float;
Tue, 23 Dec 2008 19:27:42 +0100 wenzelm renamed terminal category "float" to "float_token", to avoid name
Sat, 29 Nov 2008 13:37:13 +0100 nipkow New lexical item "float".
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, 15 Aug 2008 15:51:00 +0200 wenzelm token_kind: add Space, Comment;
Sat, 09 Aug 2008 12:28:11 +0200 wenzelm pos_of_token: Position.T;
Sat, 09 Aug 2008 00:09:35 +0200 wenzelm datatype token: maintain range, tuned representation;
Thu, 07 Aug 2008 13:45:13 +0200 wenzelm improved position handling due to SymbolPos.T;
Tue, 10 Jun 2008 16:43:26 +0200 wenzelm removed obsolete read_idents;
Mon, 28 Jan 2008 22:27:27 +0100 wenzelm basic scanners: produce symbol list instead of imploded string;
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Sat, 15 Sep 2007 19:26:28 +0200 wenzelm replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
Mon, 13 Aug 2007 18:10:22 +0200 wenzelm Lexicon.tokenize: do not appen EndToken yet;
Thu, 12 Jul 2007 00:15:41 +0200 wenzelm sys_error;
Wed, 11 Jul 2007 17:47:45 +0200 wenzelm Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
Sat, 14 Apr 2007 17:36:18 +0200 wenzelm removed redundant string_of_vname (see term.ML);
Tue, 03 Apr 2007 19:24:21 +0200 wenzelm avoid overloaded integer constants (accomodate Alice);
Fri, 15 Dec 2006 00:08:06 +0100 wenzelm avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
Tue, 12 Dec 2006 00:25:09 +0100 wenzelm read_xnum: return leading_zeros, radix;
Mon, 11 Dec 2006 21:41:03 +0100 wenzelm xstr: disallow backslashes;
Thu, 21 Sep 2006 19:04:20 +0200 wenzelm member (op =);
Wed, 02 Aug 2006 22:27:07 +0200 wenzelm renamed Syntax.indexname to Syntax.read_indexname;
Wed, 19 Jul 2006 12:12:08 +0200 wenzelm export is_tid;
Tue, 11 Jul 2006 14:21:08 +0200 wenzelm uniform treatment of num/xnum;
Tue, 11 Jul 2006 12:22:58 +0200 wenzelm tuned;
Tue, 11 Jul 2006 00:43:54 +0200 kleing hex and binary numerals (contributed by Rafal Kolanski)
Sat, 17 Jun 2006 19:38:00 +0200 wenzelm moved internal/skolem to term.ML;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Tue, 21 Mar 2006 12:18:15 +0100 wenzelm avoid polymorphic equality;
Fri, 10 Feb 2006 02:22:50 +0100 wenzelm added fixedN, constN;
Thu, 08 Dec 2005 20:16:10 +0100 wenzelm removed Syntax.deskolem;
Wed, 16 Nov 2005 17:45:35 +0100 wenzelm added deskolem;
Tue, 31 May 2005 11:53:41 +0200 wenzelm moved is_ident to General/symbol.ML;
Tue, 17 May 2005 18:10:44 +0200 wenzelm added read_variable: optional question mark on input;
Mon, 16 May 2005 10:29:15 +0200 paulson Use of IntInf.int instead of int in most numeric simprocs; avoids
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
less more (0) -120 tip