src/Pure/PIDE/markup_tree.scala
Mon, 24 Oct 2016 12:16:12 +0200 wenzelm discontinued unused / untested distinction of separate PIDE modules;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Fri, 26 Sep 2014 14:29:06 +0200 wenzelm tuned message;
Tue, 12 Aug 2014 15:46:20 +0200 wenzelm tuned;
Tue, 29 Apr 2014 13:32:13 +0200 wenzelm more systematic Isabelle output, like in classic Isabelle/ML (without markup);
Sat, 26 Apr 2014 13:07:20 +0200 wenzelm tuned signature;
Sat, 29 Mar 2014 09:24:39 +0100 wenzelm tuned -- see Text.Range.overlaps(Range);
Fri, 28 Mar 2014 21:17:47 +0100 wenzelm tuned;
Thu, 27 Mar 2014 20:28:19 +0100 wenzelm more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
Thu, 27 Mar 2014 13:00:40 +0100 wenzelm more frugal merge of markup trees: non-overlapping tree counts as empty;
Thu, 27 Mar 2014 12:11:32 +0100 wenzelm more frugal merge of markup trees: filter wrt. subsequent query;
Thu, 27 Mar 2014 11:19:31 +0100 wenzelm tuned signature;
Thu, 27 Mar 2014 10:43:43 +0100 wenzelm more careful treatment of multiple command states (eval + prints): merge content that is actually required;
Sat, 01 Mar 2014 12:07:26 +0100 wenzelm tuned signature -- more explicit Document.Elements;
Fri, 21 Feb 2014 16:14:35 +0100 wenzelm eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
Fri, 21 Feb 2014 12:07:38 +0100 wenzelm tuned -- remaining rev_markup is rather short after filter;
Thu, 20 Feb 2014 16:56:51 +0100 wenzelm clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
Thu, 20 Feb 2014 16:00:37 +0100 wenzelm cumulate/select wrt. precise elements guard;
Thu, 20 Feb 2014 14:36:17 +0100 wenzelm tuned imports;
Wed, 07 Aug 2013 19:59:58 +0200 wenzelm more elementary list structures for markup tree traversal;
Wed, 07 Aug 2013 13:46:32 +0200 wenzelm more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
Sat, 13 Jul 2013 12:39:45 +0200 wenzelm full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
Thu, 04 Apr 2013 18:20:00 +0200 wenzelm tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
Sun, 30 Dec 2012 20:15:02 +0100 wenzelm ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
Sat, 15 Dec 2012 18:30:09 +0100 wenzelm maintain subtree_elements for improved performance of cumulate operator;
Sat, 15 Dec 2012 16:59:33 +0100 wenzelm more formal class Markup_Tree.Elements;
Fri, 28 Sep 2012 22:53:18 +0200 wenzelm support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
Thu, 27 Sep 2012 19:34:31 +0200 wenzelm operations to turn markup into XML;
Thu, 27 Sep 2012 14:50:06 +0200 wenzelm tuned;
Thu, 27 Sep 2012 14:46:34 +0200 wenzelm updated to consolidated SortedMap in scala-2.9.x;
Thu, 20 Sep 2012 16:02:10 +0200 wenzelm more direct Markup_Tree.from_XML;
Thu, 20 Sep 2012 13:34:27 +0200 wenzelm more direct Markup_Tree.from_XML;
Thu, 20 Sep 2012 11:09:53 +0200 wenzelm tuned signature;
Thu, 20 Sep 2012 10:43:04 +0200 wenzelm tuned;
Tue, 18 Sep 2012 15:55:29 +0200 wenzelm recover order of stacked markup;
Fri, 10 Aug 2012 21:22:40 +0200 wenzelm tuned message;
Wed, 18 Apr 2012 16:53:00 +0200 wenzelm flat presentation of collective markup;
Mon, 27 Feb 2012 17:13:25 +0100 wenzelm prefer final ADTs -- prevent ooddities;
Tue, 10 Jan 2012 23:26:27 +0100 wenzelm clarified Isabelle_Rendering vs. physical painting;
Mon, 09 Jan 2012 23:09:03 +0100 wenzelm proper cumulation of bulk arguments;
Tue, 29 Nov 2011 21:29:53 +0100 wenzelm separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
Mon, 28 Nov 2011 22:18:19 +0100 wenzelm explicit indication of modules for independent Scala library;
Sat, 12 Nov 2011 19:44:56 +0100 wenzelm index markup elements for more efficient cumulate/select operations;
Sat, 12 Nov 2011 18:56:49 +0100 wenzelm tuned;
Sat, 12 Nov 2011 17:52:28 +0100 wenzelm more precise type;
Sat, 12 Nov 2011 17:01:58 +0100 wenzelm refined Markup_Tree implementation: stacked markup within each entry;
Sat, 12 Nov 2011 12:21:42 +0100 wenzelm tuned signature;
Sat, 12 Nov 2011 11:45:49 +0100 wenzelm tuned signature;
Fri, 11 Nov 2011 21:45:52 +0100 wenzelm added markup_cumulate operator;
Fri, 11 Nov 2011 16:06:26 +0100 wenzelm tuned;
Fri, 11 Nov 2011 15:25:22 +0100 wenzelm more abstract Markup_Tree;
Fri, 11 Nov 2011 14:24:38 +0100 wenzelm prefer statically typed Text.Markup;
Mon, 22 Aug 2011 16:12:23 +0200 wenzelm added official Text.Range.Ordering;
Sat, 09 Jul 2011 12:56:51 +0200 wenzelm tuned signature;
Thu, 23 Jun 2011 14:52:32 +0200 wenzelm explicit import java.lang.System to prevent odd scope problems;
Tue, 07 Sep 2010 23:06:52 +0200 wenzelm concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
Tue, 07 Sep 2010 22:28:58 +0200 wenzelm simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
Sun, 29 Aug 2010 15:09:11 +0200 wenzelm added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
Thu, 26 Aug 2010 11:31:21 +0200 wenzelm Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
Tue, 24 Aug 2010 21:34:38 +0200 wenzelm Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
less more (0) -60 tip