# HG changeset patch
# User aspinall
# Date 1168340989 -3600
# Node ID c874c3f13c454c8069702764575627fff254b865
# Parent  635aaa46b44d1a5904820cbe796d73adeceb3d56
Add info fatality for error messages.

diff -r 635aaa46b44d -r c874c3f13c45 src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Tue Jan 09 12:09:21 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Tue Jan 09 12:09:49 2007 +0100
@@ -44,7 +44,7 @@
     datatype messagecategory = Normal | Information | Tracing | Internal 
 
     (* Error levels *)
-    datatype fatality = Warning | Nonfatal | Fatal | Panic | Log | Debug
+    datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug
 
     (* File location *)
     type location = { descr: string option,
@@ -332,7 +332,7 @@
 
 datatype messagecategory = Normal | Information | Tracing | Internal 
 
-datatype fatality = Warning | Nonfatal | Fatal | Panic | Log | Debug
+datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug
 
 type location = { descr: string option,
 		  url: pgipurl option,
@@ -379,7 +379,8 @@
     | string_of_msgcat Tracing = "tracing"
     | string_of_msgcat Normal = "normal"   (* omitted in PGIP *)
 
-  fun string_of_fatality Warning = "warning"
+  fun string_of_fatality Info = "info"
+    | string_of_fatality Warning = "warning"
     | string_of_fatality Nonfatal = "nonfatal"
     | string_of_fatality Fatal = "fatal"
     | string_of_fatality Panic = "panic"