| Mon, 08 Mar 2021 09:11:09 +0100 |
\----- start update Isabelle2020 --> Isabelle2021
|
file | diff | annotate |
| Wed, 23 Sep 2020 15:18:07 +0200 |
\----- start update Isabelle2019 --> Isabelle2020
|
file | diff | annotate |
| Tue, 03 Sep 2019 16:10:31 +0200 |
\----- start update Isabelle2018 --> Isabelle2019
|
file | diff | annotate |
| Wed, 22 Aug 2018 14:44:15 +0200 |
\----- start update Isabelle2017 --> Isabelle2018
|
file | diff | annotate |
| Fri, 19 Jan 2018 12:49:17 +0100 |
\----- start update Isabelle2015 --> Isabelle2017
|
file | diff | annotate |
| Sat, 05 Dec 2015 16:09:41 +0100 |
switched from Isabelle2014 to Isabelle2015, intermediate state
|
file | diff | annotate |
| Fri, 02 May 2014 18:54:47 +0200 |
avoid deprecated Scala syntax;
|
file | diff | annotate |
| Fri, 02 May 2014 12:27:40 +0200 |
support URLs as well;
|
file | diff | annotate |
| Fri, 02 May 2014 12:09:02 +0200 |
reclaimed Byte_Reader from 51560e392e1b;
|
file | diff | annotate |
| Tue, 22 Apr 2014 23:57:17 +0200 |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
file | diff | annotate |
| Fri, 07 Mar 2014 16:50:42 +0100 |
tuned;
|
file | diff | annotate |
| Sun, 16 Feb 2014 13:18:08 +0100 |
tuned signature -- emphasize line-oriented aspect;
|
file | diff | annotate |
| Sat, 15 Feb 2014 14:52:51 +0100 |
partial scans via ML_Lex.tokenize_context;
|
file | diff | annotate |
| Fri, 14 Feb 2014 21:06:20 +0100 |
lexical syntax for SML (in Scala);
|
file | diff | annotate |
| Fri, 14 Feb 2014 16:25:30 +0100 |
tuned signature (in accordance to ML version);
|
file | diff | annotate |
| Fri, 14 Feb 2014 15:42:27 +0100 |
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
|
file | diff | annotate |
| Sat, 18 Jan 2014 19:24:45 +0100 |
tuned;
|
file | diff | annotate |
| Sat, 18 Jan 2014 19:15:12 +0100 |
support for nested text cartouches;
|
file | diff | annotate |
| Tue, 13 Aug 2013 20:34:46 +0200 |
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
|
file | diff | annotate |
| Thu, 08 Aug 2013 17:36:14 +0200 |
more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
|
file | diff | annotate |
| Wed, 10 Jul 2013 16:25:26 +0200 |
more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
|
file | diff | annotate |
| Thu, 23 Aug 2012 20:49:00 +0200 |
eliminated obsolete byte_reader -- theory headers + body files are parsed in full;
|
file | diff | annotate |
| Fri, 10 Aug 2012 21:53:20 +0200 |
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
|
file | diff | annotate |
| Fri, 10 Aug 2012 13:33:07 +0200 |
clarified undefined, unparsed, unfinished command spans;
|
file | diff | annotate |
| Thu, 09 Aug 2012 14:56:06 +0200 |
tuned;
|
file | diff | annotate |
| Thu, 09 Aug 2012 14:37:43 +0200 |
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
|
file | diff | annotate |
| Fri, 20 Jul 2012 22:29:25 +0200 |
more explicit java.io.{File => JFile};
|
file | diff | annotate |
| Wed, 18 Jul 2012 20:55:19 +0200 |
tuned import;
|
file | diff | annotate |
| Mon, 27 Feb 2012 17:13:25 +0100 |
prefer final ADTs -- prevent ooddities;
|
file | diff | annotate |
| Thu, 23 Feb 2012 20:40:20 +0100 |
avoid trait Addable, which is deprecated in scala-2.9.x;
|
file | diff | annotate |
| Fri, 16 Dec 2011 13:37:08 +0100 |
prefer sorting from Scala library;
|
file | diff | annotate |
| Sat, 22 Oct 2011 23:43:01 +0200 |
class Lexicon as abstract datatype;
|
file | diff | annotate |
| Thu, 07 Jul 2011 14:10:50 +0200 |
explicit indication of type Symbol.Symbol;
|
file | diff | annotate |
| Thu, 07 Jul 2011 13:48:30 +0200 |
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
|
file | diff | annotate |
| Fri, 17 Jun 2011 14:31:13 +0200 |
unconditional recovery from bad context (e.g. Quoted with malformed quoted_body);
|
file | diff | annotate |
| Thu, 16 Jun 2011 18:00:56 +0200 |
partial scans of nested comments;
|
file | diff | annotate |
| Thu, 16 Jun 2011 17:25:16 +0200 |
some support for partial scans with explicit context;
|
file | diff | annotate |
| Thu, 12 May 2011 16:28:46 +0200 |
minor adaption for scala-2.9.0.final;
|
file | diff | annotate |
| Thu, 21 Apr 2011 16:03:13 +0200 |
more robust scanning of iterated comments, such as "(* (**) (**) *)";
|
file | diff | annotate |
| Sat, 13 Nov 2010 19:21:53 +0100 |
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
|
file | diff | annotate |
| Sat, 30 Oct 2010 15:26:40 +0200 |
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
|
file | diff | annotate |
| Thu, 12 Aug 2010 17:55:23 +0200 |
more basic notion of unparsed input;
|
file | diff | annotate |
| Mon, 17 May 2010 14:23:54 +0200 |
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
|
file | diff | annotate |
| Wed, 05 May 2010 23:41:59 +0200 |
use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
|
file | diff | annotate |
| Mon, 29 Mar 2010 22:55:57 +0200 |
replaced some deprecated methods;
|
file | diff | annotate |
| Mon, 29 Mar 2010 22:43:56 +0200 |
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
|
file | diff | annotate |
| Mon, 11 Jan 2010 21:37:48 +0100 |
clarified Symbol.is_plain/is_wellformed -- is_closed was rejecting plain backslashes;
|
file | diff | annotate |
| Sun, 10 Jan 2010 17:29:09 +0100 |
tuned;
|
file | diff | annotate |
| Tue, 05 Jan 2010 16:29:03 +0100 |
more accurate scanning of bad input;
|
file | diff | annotate |
| Tue, 05 Jan 2010 15:43:44 +0100 |
tuned;
|
file | diff | annotate |
| Sun, 27 Dec 2009 22:16:41 +0100 |
quoted_content: handle escapes;
|
file | diff | annotate |
| Sun, 27 Dec 2009 21:33:35 +0100 |
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
|
file | diff | annotate |
| Tue, 22 Dec 2009 14:58:13 +0100 |
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
|
file | diff | annotate |
| Sun, 20 Dec 2009 18:02:13 +0100 |
improve performance by reordering of parser combinators;
|
file | diff | annotate |
| Sun, 20 Dec 2009 17:47:59 +0100 |
added nested comments;
|
file | diff | annotate |
| Sun, 20 Dec 2009 15:42:40 +0100 |
simplified result of keyword and symbols parser;
|
file | diff | annotate |
| Sat, 19 Dec 2009 16:51:32 +0100 |
refined some Symbol operations/signatures;
|
file | diff | annotate |
| Sat, 19 Dec 2009 11:48:11 +0100 |
indicate final state of keywords;
|
file | diff | annotate |
| Sat, 29 Aug 2009 14:31:39 +0200 |
misc tuning;
|
file | diff | annotate |
| Tue, 23 Jun 2009 17:43:51 +0200 |
moved string utilities to completion.scala;
|
file | diff | annotate |