src/Pure/General/linear_set.scala
Fri, 10 Aug 2012 20:53:16 +0200 wenzelm clarified Linear_Set.next/prev: check definedness;
Fri, 10 Aug 2012 13:15:00 +0200 wenzelm tuned;
Thu, 09 Aug 2012 21:09:24 +0200 wenzelm refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
Thu, 09 Aug 2012 19:51:29 +0200 wenzelm tuned signature;
Thu, 09 Aug 2012 19:37:42 +0200 wenzelm more direct Linear_Set.reverse, swapping orientation of the graph;
Mon, 27 Feb 2012 17:13:25 +0100 wenzelm prefer final ADTs -- prevent ooddities;
Sun, 26 Feb 2012 19:20:46 +0100 wenzelm more PIDE modules;
Thu, 23 Feb 2012 18:38:30 +0100 wenzelm streamlined abstract datatype, eliminating odd representation class;
Thu, 23 Feb 2012 18:14:58 +0100 wenzelm tuned;
Thu, 12 May 2011 16:28:46 +0200 wenzelm minor adaption for scala-2.9.0.final;
Sun, 22 Aug 2010 22:09:14 +0200 wenzelm tuned;
Tue, 17 Aug 2010 15:10:49 +0200 wenzelm added functor Linear_Set, based on former adhoc structures in document.ML;
Fri, 13 Aug 2010 17:35:28 +0200 wenzelm added get_after convenience;
Sat, 29 May 2010 17:26:02 +0200 wenzelm avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;
Mon, 24 May 2010 23:01:51 +0200 wenzelm renamed "rev" to "reverse" following usual Scala conventions;
less more (0) -15 tip