clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
discontinued obsolete "hover_message" decoration;

--- a/src/Tools/VSCode/extension/package.json	Mon Mar 06 17:48:22 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Mon Mar 06 18:28:48 2017 +0100
@@ -97,7 +97,9 @@
                 "isabelle.writeln_light_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
                 "isabelle.writeln_dark_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
                 "isabelle.information_light_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" },
-                "isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }
+                "isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" },
+                "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
+                "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }
             }
         }
     },

--- a/src/Tools/VSCode/extension/src/decorations.ts	Mon Mar 06 17:48:22 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Mon Mar 06 18:28:48 2017 +0100
@@ -32,7 +32,8 @@
 
 const dotted_colors = [
   "writeln",
-  "information"
+  "information",
+  "warning"
 ]
 
 function get_color(color: string, light: boolean): string
@@ -75,7 +76,6 @@
   for (let color of dotted_colors) {
     types["dotted_".concat(color)] = dotted(color)
   }
-  types["hover_message"] = decoration({})
 }
 
 

--- a/src/Tools/VSCode/src/server.scala	Mon Mar 06 17:48:22 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Mar 06 18:28:48 2017 +0100
@@ -300,7 +300,7 @@
     val result =
       for {
         (rendering, offset) <- rendering_offset(node_pos)
-        info <- rendering.tooltips(Rendering.tooltip_elements, Text.Range(offset, offset + 1))
+        info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1))
       } yield {
         val doc = rendering.model.content.doc
         val range = doc.range(info.range)

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Mar 06 17:48:22 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Mar 06 18:28:48 2017 +0100
@@ -30,16 +30,13 @@
   }
 
   private val dotted_colors =
-    Set(Rendering.Color.writeln, Rendering.Color.information)
+    Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning)
 
 
   /* diagnostic messages */
 
   private val message_severity =
     Map(
-      Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
-      Markup.INFORMATION -> Protocol.DiagnosticSeverity.Hint,
-      Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
       Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
       Markup.ERROR -> Protocol.DiagnosticSeverity.Error)
 
@@ -47,12 +44,14 @@
   /* markup elements */
 
   private val diagnostics_elements =
-    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
+    Markup.Elements(Markup.LEGACY, Markup.ERROR)
 
   private val dotted_elements =
-    Markup.Elements(Markup.WRITELN, Markup.INFORMATION)
+    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
 
-  private val hover_message_elements = Markup.Elements(Markup.BAD)
+  val tooltip_elements =
+    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.BAD) ++
+    Rendering.tooltip_elements
 
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
@@ -121,27 +120,7 @@
 
   /* decorations */
 
-  def hover_message: Document_Model.Decoration =
-  {
-    val results =
-      snapshot.cumulate[Command.Results](
-        model.content.text_range, Command.Results.empty,
-        VSCode_Rendering.hover_message_elements, _ =>
-          {
-            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
-            if body.nonEmpty =>
-              Some(msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body)))
-
-            case _ => None
-          })
-    val content =
-      for (Text.Info(r, msgs) <- results if !msgs.is_empty)
-      yield Text.Info(r, (for ((_, t) <- msgs.iterator) yield List(t)).toList)
-    Document_Model.Decoration("hover_message", content)
-  }
-
   def decorations: List[Document_Model.Decoration] = // list of canonical length and order
-    hover_message ::
     VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
       background(model.content.text_range, Set.empty)) :::
     VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,