| Fri, 12 Aug 2011 15:30:12 +0200 | wenzelm | allow "$" within basic path elements (NB: initial "$" refers to path variable); | changeset | files |
| Fri, 12 Aug 2011 15:28:30 +0200 | wenzelm | clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path); | changeset | files |
| Fri, 12 Aug 2011 12:03:17 +0200 | wenzelm | simplified class Thy_Header; | changeset | files |
| Fri, 12 Aug 2011 11:41:26 +0200 | wenzelm | clarified Exn.message; | changeset | files |