| Thu, 19 Aug 2010 17:40:44 +0200 | wenzelm | Markup_Tree.select: crude version of stream-based filtering; | changeset | files |
| Thu, 19 Aug 2010 17:37:13 +0200 | wenzelm | Text.Range: improved handling of singularities; | changeset | files |
| Thu, 19 Aug 2010 14:52:25 +0200 | wenzelm | tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient; | changeset | files |
| Thu, 19 Aug 2010 12:51:48 +0200 | wenzelm | moved Isar_Document to Pure/PIDE; | changeset | files |
| Thu, 19 Aug 2010 12:41:40 +0200 | wenzelm | tuned Markup_Tree, using SortedMap more carefully; | changeset | files |
| Thu, 19 Aug 2010 11:28:51 +0200 | wenzelm | Output_Position.report_text -- markup with potential "arguments"; | changeset | files |
| Thu, 19 Aug 2010 11:26:07 +0200 | wenzelm | Command.status: full XML.Tree, i.e. Markup with potential "arguments"; | changeset | files |
| Wed, 18 Aug 2010 23:44:50 +0200 | wenzelm | more efficient Markup_Tree, based on branches sorted by quasi-order; | changeset | files |