Sat, 07 Jul 2007 00:15:03 +0200 | wenzelm | simplified pretty token metric: type int; | changeset | files |
Sat, 07 Jul 2007 00:15:02 +0200 | wenzelm | simplified pretty token metric: type int; | changeset | files |
Sat, 07 Jul 2007 00:15:02 +0200 | wenzelm | moved General/xml.ML to Tools/xml.ML; | changeset | files |
Sat, 07 Jul 2007 00:15:00 +0200 | wenzelm | tuned; | changeset | files |
Sat, 07 Jul 2007 00:14:59 +0200 | wenzelm | simplified output mode setup; | changeset | files |
Sat, 07 Jul 2007 00:14:58 +0200 | wenzelm | added print_mode setup: indent and markup; | changeset | files |