# HG changeset patch
# User wenzelm
# Date 1574684911 -3600
# Node ID 03afc82522255778a5f4506307c3413319988986
# Parent  a21a29de5f57ed758c474459b935ea062f06ef03
support for output messages;

diff -r a21a29de5f57 -r 03afc8252225 src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Mon Nov 25 12:41:52 2019 +0100
+++ b/src/Pure/Isar/document_structure.scala	Mon Nov 25 13:28:31 2019 +0100
@@ -27,6 +27,9 @@
   def is_document_command(keywords: Keyword.Keywords, command: Command): Boolean =
     command.span.is_kind(keywords, Keyword.document, false)
 
+  def is_diag_command(keywords: Keyword.Keywords, command: Command): Boolean =
+    command.span.is_kind(keywords, Keyword.diag, false)
+
   def is_heading_command(command: Command): Boolean =
     proper_heading_level(command).isDefined
 
diff -r a21a29de5f57 -r 03afc8252225 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Nov 25 12:41:52 2019 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Nov 25 13:28:31 2019 +0100
@@ -150,6 +150,14 @@
   def is_exported(msg: XML.Tree): Boolean =
     is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
 
+  def message_text(msg: XML.Tree): String =
+  {
+    val text = Pretty.string_of(List(msg))
+    if (is_warning(msg) || is_legacy(msg)) Library.prefix_lines("### ", text)
+    else if (is_error(msg)) Library.prefix_lines("*** ", text)
+    else text
+  }
+
 
   /* breakpoints */