Sun, 22 Aug 2010 22:28:24 +0200 | wenzelm | tuned Markup_Tree.+ : slightly more expensive version to rebuild rest avoids crash of RedBlack.scala:120 (version Scala 2.8.0), e.g. on the following input: | changeset | files |
Sun, 22 Aug 2010 22:09:14 +0200 | wenzelm | tuned; | changeset | files |
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 |