diff --git a/src/Pure/Isar/document_structure.scala b/src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala
+++ b/src/Pure/Isar/document_structure.scala
@@ -1,221 +1,224 @@
 /*  Title:      Pure/Isar/document_structure.scala
     Author:     Makarius
 
 Overall document structure.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 
 object Document_Structure
 {
   /** general structure **/
 
   sealed abstract class Document { def length: Int }
   case class Block(name: String, text: String, body: List[Document]) extends Document
   { val length: Int = (0 /: body)(_ + _.length) }
   case class Atom(length: Int) extends Document
 
   def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
     command.span.is_kind(keywords,
       kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
 
   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
 
   def proper_heading_level(command: Command): Option[Int] =
     command.span.name match {
       case Thy_Header.CHAPTER => Some(0)
       case Thy_Header.SECTION => Some(1)
       case Thy_Header.SUBSECTION => Some(2)
       case Thy_Header.SUBSUBSECTION => Some(3)
       case Thy_Header.PARAGRAPH => Some(4)
       case Thy_Header.SUBPARAGRAPH => Some(5)
       case _ => None
     }
 
   def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
     proper_heading_level(command) orElse
       (if (is_theory_command(keywords, command)) Some(6) else None)
 
 
 
   /** context blocks **/
 
   def parse_blocks(
     syntax: Outer_Syntax,
     node_name: Document.Node.Name,
     text: CharSequence): List[Document] =
   {
     def is_plain_theory(command: Command): Boolean =
       is_theory_command(syntax.keywords, command) &&
       !command.span.is_begin && !command.span.is_end
 
 
     /* stack operations */
 
     def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
 
     var stack: List[(Command, mutable.ListBuffer[Document])] =
       List((Command.empty, buffer()))
 
     def open(command: Command) { stack = (command, buffer()) :: stack }
 
     def close(): Boolean =
       stack match {
         case (command, body) :: (_, body2) :: _ =>
           body2 += Block(command.span.name, command.source, body.toList)
           stack = stack.tail
           true
         case _ =>
           false
       }
 
     def flush() { if (is_plain_theory(stack.head._1)) close() }
 
     def result(): List[Document] =
     {
       while (close()) { }
       stack.head._2.toList
     }
 
     def add(command: Command)
     {
       if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
       else if (command.span.is_end) { flush(); close() }
 
       stack.head._2 += Atom(command.source.length)
     }
 
 
     /* result structure */
 
     val spans = syntax.parse_spans(text)
     spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
     result()
   }
 
 
 
   /** section headings **/
 
   trait Item
   {
     def name: String = ""
     def source: String = ""
     def heading_level: Option[Int] = None
   }
 
   object No_Item extends Item
 
   class Sections(keywords: Keyword.Keywords)
   {
     private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
 
     private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
       List((0, No_Item, buffer()))
 
     @tailrec private def close(level: Int => Boolean)
     {
       stack match {
         case (lev, item, body) :: (_, _, body2) :: _ if level(lev) =>
           body2 += Block(item.name, item.source, body.toList)
           stack = stack.tail
           close(level)
         case _ =>
       }
     }
 
     def result(): List[Document] =
     {
       close(_ => true)
       stack.head._3.toList
     }
 
     def add(item: Item)
     {
       item.heading_level match {
         case Some(i) =>
           close(_ > i)
           stack = (i + 1, item, buffer()) :: stack
         case None =>
       }
       stack.head._3 += Atom(item.source.length)
     }
   }
 
 
   /* outer syntax sections */
 
   private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item
   {
     override def name: String = command.span.name
     override def source: String = command.source
     override def heading_level: Option[Int] = Document_Structure.heading_level(keywords, command)
   }
 
   def parse_sections(
     syntax: Outer_Syntax,
     node_name: Document.Node.Name,
     text: CharSequence): List[Document] =
   {
     val sections = new Sections(syntax.keywords)
 
     for { span <- syntax.parse_spans(text) } {
       sections.add(
         new Command_Item(syntax.keywords,
           Command(Document_ID.none, node_name, Command.no_blobs, span)))
     }
     sections.result()
   }
 
 
   /* ML sections */
 
   private class ML_Item(token: ML_Lex.Token, level: Option[Int]) extends Item
   {
     override def source: String = token.source
     override def heading_level: Option[Int] = level
   }
 
   def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] =
   {
     val sections = new Sections(Keyword.Keywords.empty)
     val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None)
 
     var context: Scan.Line_Context = Scan.Finished
     for (line <- Library.separated_chunks(_ == '\n', text)) {
       val (toks, next_context) = ML_Lex.tokenize_line(SML, line, context)
       val level =
         toks.filterNot(_.is_space) match {
           case List(tok) if tok.is_comment =>
             val s = tok.source
             if (Codepoint.iterator(s).exists(c => Character.isLetter(c) || Character.isDigit(c)))
             {
               if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
               else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
               else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
               else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
               else None
             }
             else None
           case _ => None
         }
       if (level.isDefined && context == Scan.Finished && next_context == Scan.Finished)
         toks.foreach(tok => sections.add(new ML_Item(tok, if (tok.is_comment) level else None)))
       else
         toks.foreach(tok => sections.add(new ML_Item(tok, None)))
 
       sections.add(nl)
       context = next_context
     }
     sections.result()
   }
 }
diff --git a/src/Pure/PIDE/protocol.scala b/src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala
+++ b/src/Pure/PIDE/protocol.scala
@@ -1,373 +1,381 @@
 /*  Title:      Pure/PIDE/protocol.scala
     Author:     Makarius
 
 Protocol message formats for interactive proof documents.
 */
 
 package isabelle
 
 
 object Protocol
 {
   /* document editing */
 
   object Commands_Accepted
   {
     def unapply(text: String): Option[List[Document_ID.Command]] =
       try { Some(space_explode(',', text).map(Value.Long.parse)) }
       catch { case ERROR(_) => None }
 
     val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED)))
   }
 
   object Assign_Update
   {
     def unapply(text: String)
       : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
     {
       try {
         import XML.Decode._
         def decode_upd(body: XML.Body): (Long, List[Long]) =
           space_explode(',', string(body)).map(Value.Long.parse) match {
             case a :: bs => (a, bs)
             case _ => throw new XML.XML_Body(body)
           }
         Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
         case _: XML.Error => None
       }
     }
   }
 
   object Removed
   {
     def unapply(text: String): Option[List[Document_ID.Version]] =
       try {
         import XML.Decode._
         Some(list(long)(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
         case _: XML.Error => None
       }
   }
 
 
   /* command timing */
 
   object Command_Timing
   {
     def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
       props match {
         case Markup.COMMAND_TIMING :: args =>
           (args, args) match {
             case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
             case _ => None
           }
         case _ => None
       }
   }
 
 
   /* theory timing */
 
   object Theory_Timing
   {
     def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
       props match {
         case Markup.THEORY_TIMING :: args =>
           (args, args) match {
             case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
             case _ => None
           }
         case _ => None
       }
   }
 
 
   /* result messages */
 
   def is_result(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.RESULT, _), _) => true
       case _ => false
     }
 
   def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.TRACING, _), _) => true
       case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_state(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.STATE, _), _) => true
       case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_information(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
       case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_writeln(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WRITELN, _), _) => true
       case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true
       case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_legacy(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.LEGACY, _), _) => true
       case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_error(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.ERROR, _), _) => true
       case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_inlined(msg: XML.Tree): Boolean =
     !(is_result(msg) || is_tracing(msg) || is_state(msg))
 
   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 */
 
   object ML_Breakpoint
   {
     def unapply(tree: XML.Tree): Option[Long] =
     tree match {
       case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
       case _ => None
     }
   }
 
 
   /* dialogs */
 
   object Dialog_Args
   {
     def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
       (props, props, props) match {
         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
           Some((id, serial, result))
         case _ => None
       }
   }
 
   object Dialog
   {
     def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
       tree match {
         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
           Some((id, serial, result))
         case _ => None
       }
   }
 
   object Dialog_Result
   {
     def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
     {
       val props = Position.Id(id) ::: Markup.Serial(serial)
       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
     }
 
     def unapply(tree: XML.Tree): Option[String] =
       tree match {
         case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
         case _ => None
       }
   }
 }
 
 
 trait Protocol
 {
   /* protocol commands */
 
   def protocol_command_raw(name: String, args: List[Bytes]): Unit
   def protocol_command_args(name: String, args: List[String])
   def protocol_command(name: String, args: String*): Unit
 
 
   /* options */
 
   def options(opts: Options): Unit =
     protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
 
 
   /* session base */
 
   private def encode_table(table: List[(String, String)]): String =
   {
     import XML.Encode._
     Symbol.encode_yxml(list(pair(string, string))(table))
   }
 
   private def encode_list(lst: List[String]): String =
   {
     import XML.Encode._
     Symbol.encode_yxml(list(string)(lst))
   }
 
   private def encode_sessions(lst: List[(String, Position.T)]): String =
   {
     import XML.Encode._
     Symbol.encode_yxml(list(pair(string, properties))(lst))
   }
 
   def session_base(resources: Resources)
   {
     protocol_command("Prover.init_session_base",
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),
       encode_list(resources.session_base.doc_names),
       encode_table(resources.session_base.global_theories.toList),
       encode_list(resources.session_base.loaded_theories.keys))
   }
 
 
   /* interned items */
 
   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes))
 
   private def encode_command(command: Command): (String, String, String, String, List[String]) =
   {
     import XML.Encode._
 
     val blobs_yxml =
     {
       val encode_blob: T[Command.Blob] =
         variant(List(
           { case Exn.Res((a, b)) =>
               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
 
       Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     }
 
     val toks_yxml =
     {
       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
       Symbol.encode_yxml(list(encode_tok)(command.span.content))
     }
     val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source))
 
     (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources)
   }
 
   def define_command(command: Command)
   {
     val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command)
     protocol_command_args(
       "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources)
   }
 
   def define_commands(commands: List[Command])
   {
     protocol_command_args("Document.define_commands",
       commands.map(command =>
       {
         import XML.Encode._
         val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command)
         val body =
           pair(string, pair(string, pair(string, pair(string, list(string)))))(
             command_id, (name, (blobs_yxml, (toks_yxml, toks_sources))))
         YXML.string_of_body(body)
       }))
   }
 
   def define_commands_bulk(commands: List[Command])
   {
     val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
     irregular.foreach(define_command(_))
     regular match {
       case Nil =>
       case List(command) => define_command(command)
       case _ => define_commands(regular)
     }
   }
 
 
   /* execution */
 
   def discontinue_execution(): Unit =
     protocol_command("Document.discontinue_execution")
 
   def cancel_exec(id: Document_ID.Exec): Unit =
     protocol_command("Document.cancel_exec", Document_ID(id))
 
 
   /* document versions */
 
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
   {
     val consolidate_yxml =
     {
       import XML.Encode._
       Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
     }
     val edits_yxml =
     {
       import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
         variant(List(
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val master_dir = File.standard_url(name.master_dir)
               val imports = header.imports.map(_.node)
               val keywords =
                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
               (Nil,
                 pair(string, pair(string, pair(list(string), pair(list(pair(string,
                     pair(pair(string, list(string)), list(string)))), list(string)))))(
                 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(string, list(string))))(c.dest)) }))
       edits.map({ case (name, edit) =>
         Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) })
     }
     protocol_command_args("Document.update",
       Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml)
   }
 
   def remove_versions(versions: List[Document.Version])
   {
     val versions_yxml =
     { import XML.Encode._
       Symbol.encode_yxml(list(long)(versions.map(_.id))) }
     protocol_command("Document.remove_versions", versions_yxml)
   }
 
 
   /* dialog via document content */
 
   def dialog_result(serial: Long, result: String): Unit =
     protocol_command("Document.dialog_result", Value.Long(serial), result)
 }