# HG changeset patch
# User aspinall
# Date 1184145924 -7200
# Node ID d74a16b84e0560c47618feca83d27cde92749d7c
# Parent  15839159f8b6e11fe26eec724fe32a910c4f49c2
Track schema changes: merge messagecategory with area attributes

diff -r 15839159f8b6 -r d74a16b84e05 src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Wed Jul 11 11:25:21 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Wed Jul 11 11:25:24 2007 +0200
@@ -36,12 +36,8 @@
     (* Representation error in reading/writing PGIP *)
     exception PGIP of string
 
-
     (* Interface areas for message output *)
-    datatype displayarea = Status | Message | Display | Other of string
-
-    (* Kinds of message output (influence display behaviour) *)
-    datatype messagecategory = Normal | Information | Tracing | Internal 
+    datatype displayarea = Status | Message | Display | Tracing | Internal | Other of string
 
     (* Error levels *)
     datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug
@@ -86,7 +82,6 @@
     val pgval_to_string   : pgipval -> string
 
     val attrs_of_displayarea : displayarea -> XML.attributes
-    val attrs_of_messagecategory : messagecategory -> XML.attributes
     val attrs_of_fatality : fatality -> XML.attributes
     val attrs_of_location : location -> XML.attributes
     val location_of_attrs : XML.attributes -> location (* raises PGIP *)
@@ -329,9 +324,7 @@
 
 type pgipurl = Path.T    (* URLs: only local files *)
 
-datatype displayarea = Status | Message | Display | Other of string
-
-datatype messagecategory = Normal | Information | Tracing | Internal 
+datatype displayarea = Status | Message | Display | Tracing | Internal | Other of string
 
 datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug
 
@@ -374,13 +367,10 @@
   fun string_of_area Status = "status"
     | string_of_area Message = "message"
     | string_of_area Display = "display"
+    | string_of_area Tracing = "tracing"
+    | string_of_area Internal = "internal"
     | string_of_area (Other s) = s
 
-  fun string_of_msgcat Internal = "internal"
-    | string_of_msgcat Information = "information"
-    | string_of_msgcat Tracing = "tracing"
-    | string_of_msgcat Normal = "normal"   (* omitted in PGIP *)
-
   fun string_of_fatality Info = "info"
     | string_of_fatality Warning = "warning"
     | string_of_fatality Nonfatal = "nonfatal"
@@ -391,11 +381,6 @@
 in
   fun attrs_of_displayarea area = [("area", string_of_area area)]
 
-  fun attrs_of_messagecategory msgcat = 
-      case msgcat of 
-	  Normal => []
-	| _ => [("messagecategory", string_of_msgcat msgcat)]
-
   fun attrs_of_fatality fatality = [("fatality", string_of_fatality fatality)]
 
   fun attrs_of_location ({ descr, url, line, column, char, length }:location) =