# 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"