| Sun, 22 Aug 2010 20:25:15 +0200 | wenzelm | tuned signature; | changeset | files |
| Sun, 22 Aug 2010 20:11:17 +0200 | wenzelm | simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports); | changeset | files |
| Sun, 22 Aug 2010 19:55:41 +0200 | wenzelm | proper range for hyperlinks and tooltips, using original markup information; | changeset | files |
| 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 |