Mon, 23 Jul 2007 19:45:47 +0200 | wenzelm | marked some CRITICAL sections; | changeset | files |
Mon, 23 Jul 2007 19:45:46 +0200 | wenzelm | marked some CRITICAL sections; | changeset | files |
Mon, 23 Jul 2007 19:45:45 +0200 | wenzelm | depth flag: plain bool ref; | changeset | files |
Mon, 23 Jul 2007 19:45:44 +0200 | wenzelm | eliminated transform_failure (to avoid critical section for main transactions); | changeset | files |
Mon, 23 Jul 2007 16:45:04 +0200 | wenzelm | setmp_noncritical (assumes outermost control); | changeset | files |
Mon, 23 Jul 2007 16:45:03 +0200 | wenzelm | PrintMode.with_modes; | changeset | files |