src/Pure/PIDE/markup.ML
changeset 57975 c657c68a60ab
parent 57594 037f3b251df5
child 58048 aa6296d09e0e
     1.1 --- a/src/Pure/PIDE/markup.ML	Wed Aug 13 20:21:04 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Fri Aug 15 13:39:59 2014 +0200
     1.3 @@ -156,6 +156,7 @@
     1.4    val tracingN: string
     1.5    val warningN: string
     1.6    val errorN: string
     1.7 +  val systemN: string
     1.8    val protocolN: string
     1.9    val legacyN: string val legacy: T
    1.10    val promptN: string val prompt: T
    1.11 @@ -527,6 +528,7 @@
    1.12  val tracingN = "tracing";
    1.13  val warningN = "warning";
    1.14  val errorN = "error";
    1.15 +val systemN = "system";
    1.16  val protocolN = "protocol";
    1.17  
    1.18  val (legacyN, legacy) = markup_elem "legacy";