Sun, 29 Jul 2007 17:28:57 +0200 | wenzelm | critical: improved diagostics; | changeset | files |
Sun, 29 Jul 2007 17:28:56 +0200 | wenzelm | tuned msg; | changeset | files |
Sun, 29 Jul 2007 17:28:55 +0200 | wenzelm | NAMED_CRITICAL; | changeset | files |
Sun, 29 Jul 2007 16:00:06 +0200 | wenzelm | removed obsolete Output.ML_errors/toplevel_errors; | changeset | files |
Sun, 29 Jul 2007 16:00:05 +0200 | wenzelm | removed obsolete Output.ML_errors/toplevel_errors; | changeset | files |
Sun, 29 Jul 2007 16:00:04 +0200 | wenzelm | added TOPLEVEL_ERROR (simplified version from output.ML); | changeset | files |