src/Pure/General/scan.scala
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Thu, 08 Jan 2015 20:56:39 +0100 wenzelm tuned;
Mon, 01 Dec 2014 15:21:49 +0100 wenzelm more merge operations;
Wed, 01 Oct 2014 21:00:49 +0200 wenzelm actually finish after closing, e.g. relevant for consecutive (**)(**);
Fri, 02 May 2014 18:54:47 +0200 wenzelm avoid deprecated Scala syntax;
Fri, 02 May 2014 12:27:40 +0200 wenzelm support URLs as well;
Fri, 02 May 2014 12:09:02 +0200 wenzelm reclaimed Byte_Reader from 51560e392e1b;
Tue, 22 Apr 2014 23:57:17 +0200 wenzelm avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
Fri, 07 Mar 2014 16:50:42 +0100 wenzelm tuned;
Sun, 16 Feb 2014 13:18:08 +0100 wenzelm tuned signature -- emphasize line-oriented aspect;
Sat, 15 Feb 2014 14:52:51 +0100 wenzelm partial scans via ML_Lex.tokenize_context;
Fri, 14 Feb 2014 21:06:20 +0100 wenzelm lexical syntax for SML (in Scala);
Fri, 14 Feb 2014 16:25:30 +0100 wenzelm tuned signature (in accordance to ML version);
Fri, 14 Feb 2014 15:42:27 +0100 wenzelm tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
Sat, 18 Jan 2014 19:24:45 +0100 wenzelm tuned;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Tue, 13 Aug 2013 20:34:46 +0200 wenzelm discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
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;
Thu, 23 Aug 2012 20:49:00 +0200 wenzelm eliminated obsolete byte_reader -- theory headers + body files are parsed in full;
Fri, 10 Aug 2012 21:53:20 +0200 wenzelm more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
Fri, 10 Aug 2012 13:33:07 +0200 wenzelm clarified undefined, unparsed, unfinished command spans;
Thu, 09 Aug 2012 14:56:06 +0200 wenzelm tuned;
Thu, 09 Aug 2012 14:37:43 +0200 wenzelm refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
Fri, 20 Jul 2012 22:29:25 +0200 wenzelm more explicit java.io.{File => JFile};
Wed, 18 Jul 2012 20:55:19 +0200 wenzelm tuned import;
Mon, 27 Feb 2012 17:13:25 +0100 wenzelm prefer final ADTs -- prevent ooddities;
Thu, 23 Feb 2012 20:40:20 +0100 wenzelm avoid trait Addable, which is deprecated in scala-2.9.x;
Fri, 16 Dec 2011 13:37:08 +0100 wenzelm prefer sorting from Scala library;
Sat, 22 Oct 2011 23:43:01 +0200 wenzelm class Lexicon as abstract datatype;
less more (0) -50 -30 tip