--- 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) =