more uniform treatment of input/output wrt. client;
support for diagnistic messages;
misc tuning;

--- a/src/Pure/PIDE/line.scala	Wed Dec 28 11:28:31 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 16:45:00 2016 +0100
@@ -123,6 +123,11 @@
       move(offset, 0, lines)
     }
 
+    def range(text_range: Text.Range, length: Length = Length): Range =
+      Range(
+        position(text_range.start, length),
+        position(text_range.stop, length))
+
     def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
     {
       val l = pos.line

--- a/src/Tools/VSCode/etc/options	Wed Dec 28 11:28:31 2016 +0100
+++ b/src/Tools/VSCode/etc/options	Wed Dec 28 16:45:00 2016 +0100
@@ -1,7 +1,10 @@
 (* :mode=isabelle-options: *)
 
 option vscode_tooltip_margin : int = 60
-  -- "margin for tooltip pretty-printing"
+  -- "margin for pretty-printing of tooltips"
+
+option vscode_diagnostics_margin : int = 80
+  -- "margin for pretty-printing of diagnostic messages"
 
 option vscode_timing_threshold : real = 0.1
   -- "default threshold for timing display (seconds)"

--- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 11:28:31 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 16:45:00 2016 +0100
@@ -13,8 +13,9 @@
 
 
 case class Document_Model(
-  session: Session, doc: Line.Document, node_name: Document.Node.Name,
-  changed: Boolean = true)
+  session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Length,
+  changed: Boolean = true,
+  published_diagnostics: List[Text.Info[Command.Results]] = Nil)
 {
   /* header */
 
@@ -48,10 +49,21 @@
   def unchanged: Document_Model = if (changed) copy(changed = false) else this
 
 
+  /* diagnostics */
+
+  def publish_diagnostics(rendering: VSCode_Rendering)
+    : Option[(List[Text.Info[Command.Results]], Document_Model)] =
+  {
+    val diagnostics = rendering.diagnostics
+    if (diagnostics == published_diagnostics) None
+    else Some(diagnostics, copy(published_diagnostics = diagnostics))
+  }
+
+
   /* snapshot and rendering */
 
   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
 
-  def rendering(options: Options, text_length: Length): VSCode_Rendering =
-    new VSCode_Rendering(this, snapshot(), options, text_length, session.resources)
+  def rendering(options: Options): VSCode_Rendering =
+    new VSCode_Rendering(this, snapshot(), options, session.resources)
 }

--- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 11:28:31 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 16:45:00 2016 +0100
@@ -88,7 +88,8 @@
 
   sealed case class State(
     session: Option[Session] = None,
-    models: Map[String, Document_Model] = Map.empty)
+    models: Map[String, Document_Model] = Map.empty,
+    pending_output: Set[Document.Node.Name] = Set.empty)
 }
 
 class Server(
@@ -109,11 +110,68 @@
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
       model <- state.value.models.get(node_pos.name)
-      rendering = model.rendering(options, text_length)
+      rendering = model.rendering(options)
       offset <- model.doc.offset(node_pos.pos, text_length)
     } yield (rendering, offset)
 
 
+  /* input from client */
+
+  private val delay_input =
+    Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
+      state.change(st =>
+        {
+          val changed = (for { entry <- st.models.iterator if entry._2.changed } yield entry).toList
+          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
+          session.update(Document.Blobs.empty, edits)
+          st.copy(
+            models = (st.models /: changed)({ case (ms, (uri, m)) => ms + (uri -> m.unchanged) }))
+        })
+    }
+
+  def update_document(uri: String, text: String)
+  {
+    state.change(st =>
+      {
+        val node_name = resources.node_name(uri)
+        val model = Document_Model(session, Line.Document(text), node_name, text_length)
+        st.copy(models = st.models + (uri -> model))
+      })
+    delay_input.invoke()
+  }
+
+
+  /* output to client */
+
+  private val commands_changed =
+    Session.Consumer[Session.Commands_Changed](getClass.getName) {
+      case changed =>
+        state.change(st => st.copy(pending_output = st.pending_output ++ changed.nodes))
+        delay_output.invoke()
+    }
+
+  private val delay_output =
+    Standard_Thread.delay_last(options.seconds("editor_update_delay")) {
+      state.change(st =>
+        {
+          val changed_iterator =
+            for {
+              node_name <- st.pending_output.iterator
+              uri = node_name.node
+              model <- st.models.get(uri)
+              rendering = model.rendering(options)
+              (diagnostics, model1) <- model.publish_diagnostics(rendering)
+            } yield {
+              channel.diagnostics(uri, rendering.diagnostics_output(diagnostics))
+              (uri, model1)
+            }
+          st.copy(
+            models = (st.models /: changed_iterator) { case (ms, (uri, m)) => ms + (uri -> m) },
+            pending_output = Set.empty)
+        })
+    }
+
+
   /* init and exit */
 
   def init(id: Protocol.Id)
@@ -156,6 +214,8 @@
         }
       session.phase_changed += session_phase
 
+      session.commands_changed += commands_changed
+
       session.start(receiver =>
         Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
           modes = modes, receiver = receiver))
@@ -181,7 +241,10 @@
               case _ =>
             }
           session.phase_changed += session_phase
+          session.commands_changed -= commands_changed
           session.stop()
+          delay_input.revoke()
+          delay_output.revoke()
           st.copy(session = None)
       })
   }
@@ -192,35 +255,6 @@
   }
 
 
-  /* document management */
-
-  private val delay_flush =
-    Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
-      state.change(st =>
-        {
-          val models = st.models
-          val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList
-          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
-          val models1 =
-            (models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) })
-
-          session.update(Document.Blobs.empty, edits)
-          st.copy(models = models1)
-        })
-    }
-
-  def update_document(uri: String, text: String)
-  {
-    state.change(st =>
-      {
-        val node_name = resources.node_name(uri)
-        val model = Document_Model(session, Line.Document(text), node_name)
-        st.copy(models = st.models + (uri -> model))
-      })
-    delay_flush.invoke()
-  }
-
-
   /* hover */
 
   def hover(id: Protocol.Id, node_pos: Line.Node_Position)
@@ -231,10 +265,9 @@
         info <- rendering.tooltip(Text.Range(offset, offset + 1))
       } yield {
         val doc = rendering.model.doc
-        val start = doc.position(info.range.start, text_length)
-        val stop = doc.position(info.range.stop, text_length)
+        val range = doc.range(info.range, text_length)
         val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
-        (Line.Range(start, stop), List("```\n" + s + "\n```"))  // FIXME proper content format
+        (range, List("```\n" + s + "\n```"))  // FIXME proper content format
       }
     channel.write(Protocol.Hover.reply(id, result))
   }

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 11:28:31 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 16:45:00 2016 +0100
@@ -12,6 +12,24 @@
 
 object VSCode_Rendering
 {
+  /* diagnostic messages */
+
+  private val message_severity =
+    Map(
+      Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
+      Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
+      Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
+      Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
+      Markup.ERROR -> Protocol.DiagnosticSeverity.Error,
+      Markup.BAD -> Protocol.DiagnosticSeverity.Error)
+
+
+  /* markup elements */
+
+  private val diagnostics_elements =
+    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
+      Markup.BAD)
+
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
 }
@@ -20,10 +38,37 @@
     val model: Document_Model,
     snapshot: Document.Snapshot,
     options: Options,
-    text_length: Length,
     resources: Resources)
   extends Rendering(snapshot, options, resources)
 {
+  /* diagnostics */
+
+  def diagnostics: List[Text.Info[Command.Results]] =
+    snapshot.cumulate[Command.Results](
+      Text.Range.full, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
+      {
+        case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
+        if body.nonEmpty => Some(res + (i -> msg))
+
+        case _ => None
+      })
+
+  val diagnostics_margin = options.int("vscode_diagnostics_margin")
+
+  def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
+  {
+    (for {
+      Text.Info(text_range, res) <- results.iterator
+      range = model.doc.range(text_range, model.text_length)
+      (_, XML.Elem(Markup(name, _), body)) <- res.iterator
+    } yield {
+      val message = Pretty.string_of(body, margin = diagnostics_margin)
+      val severity = VSCode_Rendering.message_severity.get(name)
+      Protocol.Diagnostic(range, message, severity = severity)
+    }).toList
+  }
+
+
   /* tooltips */
 
   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
@@ -45,7 +90,8 @@
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)
             val doc = Line.Document(text)
-            def position(offset: Symbol.Offset) = doc.position(chunk.decode(offset), text_length)
+            def position(offset: Symbol.Offset) =
+              doc.position(chunk.decode(offset), model.text_length)
             Line.Range(position(range.start), position(range.stop))
           case _ =>
             Line.Range(Line.Position((line1 - 1) max 0))