--- 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
--- 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 */