| Sat, 09 Apr 2016 20:14:00 +0200 | wenzelm | proper signature for structure; | changeset | files |
| Sat, 09 Apr 2016 20:07:10 +0200 | wenzelm | tuned signature; | changeset | files |
| Sat, 09 Apr 2016 19:38:25 +0200 | wenzelm | proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML; | changeset | files |
| Sat, 09 Apr 2016 19:30:15 +0200 | wenzelm | support ROOT0.ML as well -- independently of ROOT.ML; | changeset | files |
| Sat, 09 Apr 2016 19:09:11 +0200 | wenzelm | flags as in 'ML' command; | changeset | files |
| Sat, 09 Apr 2016 16:16:05 +0200 | wenzelm | shared output primitives of physical/virtual Pure; | changeset | files |