# HG changeset patch
# User aspinall
# Date 1167930570 -3600
# Node ID 358525557580fcf025fe1fe97fffbcf0ea6b50a4
# Parent  0cf192e489e2565cdc63e8e87d1b8e7cc770f6dd
Add warning fatality

diff -r 0cf192e489e2 -r 358525557580 src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Thu Jan 04 17:55:12 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Thu Jan 04 18:09:30 2007 +0100
@@ -44,7 +44,7 @@
     datatype messagecategory = Normal | Information | Tracing | Internal 
 
     (* Error levels *)
-    datatype fatality = Nonfatal | Fatal | Panic | Log | Debug
+    datatype fatality = Warning | Nonfatal | Fatal | Panic | Log | Debug
 
     (* File location *)
     type location = { descr: string option,
@@ -330,7 +330,7 @@
 
 datatype messagecategory = Normal | Information | Tracing | Internal 
 
-datatype fatality = Nonfatal | Fatal | Panic | Log | Debug
+datatype fatality = Warning | Nonfatal | Fatal | Panic | Log | Debug
 
 type location = { descr: string option,
 		  url: pgipurl option,
@@ -375,7 +375,8 @@
     | string_of_msgcat Tracing = "tracing"
     | string_of_msgcat Normal = "normal"   (* omitted in PGIP *)
 
-  fun string_of_fatality Nonfatal = "nonfatal"
+  fun string_of_fatality Warning = "warning"
+    | string_of_fatality Nonfatal = "nonfatal"
     | string_of_fatality Fatal = "fatal"
     | string_of_fatality Panic = "panic"
     | string_of_fatality Log = "log"