Sun, 22 Aug 2010 19:53:20 +0200 | wenzelm | tuned signature; | changeset | files |
Sun, 22 Aug 2010 19:33:01 +0200 | wenzelm | misc tuning and simplification; | changeset | files |
Sun, 22 Aug 2010 18:46:16 +0200 | wenzelm | renamed Markup_Tree.Node to Text.Info; | changeset | files |
Sun, 22 Aug 2010 16:43:20 +0200 | wenzelm | removed obsolete Markup_Tree.flatten/filter; | changeset | files |