# HG changeset patch
# User wenzelm
# Date 1086800207 -7200
# Node ID 396a1f4b9c14f5e6a45b7af9200bd9853603c0ba
# Parent  f145696d4bb58b997a7b9e7c55048c83140da90e
tuned comment;

diff -r f145696d4bb5 -r 396a1f4b9c14 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Wed Jun 09 18:56:38 2004 +0200
+++ b/src/Pure/General/output.ML	Wed Jun 09 18:56:47 2004 +0200
@@ -3,7 +3,7 @@
     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Output channels and diagnostics messages.
+Output channels and diagnostic messages.
 *)
 
 signature BASIC_OUTPUT =
@@ -110,6 +110,7 @@
 fun error_msg s = ! error_fn (output s);
 fun panic_msg s = ! panic_fn (output s);
 
+
 (* add_mode *)
 
 fun add_mode name m =
@@ -118,7 +119,7 @@
   modes := Symtab.update ((name, m), ! modes));
 
 
-(* output error message and abort to top level, or panic & exit *)
+(* produce errors *)
 
 fun error s = (error_msg s; raise ERROR);
 fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
@@ -192,7 +193,7 @@
   if flag then
     let val start = startTiming()
         val result = f ()
-    in warning (endTiming start);  result end
+    in warning (endTiming start); result end
   else f ();
 
 (*unconditional timing function*)