# HG changeset patch
# User wenzelm
# Date 1482954148 -3600
# Node ID 1d645e6efd89e1786c4708cd436a66dd2a03eecd
# Parent  ef0a5fd30f3b8a56f103a70dbc5dfbed7d9f0eab# Parent  92bcb79a465e02cabaa11fe106c1e38e0dc3a738
merged

diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/General/codepoint.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -25,7 +25,7 @@
 
   def length(s: String): Int = iterator(s).length
 
-  trait Length extends isabelle.Length
+  trait Length extends Text.Length
   {
     protected def codepoint_length(c: Int): Int = 1
 
@@ -34,7 +34,7 @@
 
     def offset(s: String, i: Int): Option[Text.Offset] =
     {
-      if (i <= 0 || s.forall(_ < 0x80)) isabelle.Length.offset(s, i)
+      if (i <= 0 || s.forall(_ < 0x80)) Text.Length.offset(s, i)
       else {
         val length = s.length
         var offset = 0
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/General/length.scala
--- a/src/Pure/General/length.scala	Wed Dec 28 17:22:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-/*  Title:      Pure/General/length.scala
-    Author:     Makarius
-
-Text length wrt. encoding.
-*/
-
-package isabelle
-
-
-trait Length
-{
-  def apply(text: String): Int
-  def offset(text: String, i: Int): Option[Text.Offset]
-}
-
-object Length extends Length
-{
-  def apply(text: String): Int = text.length
-  def offset(text: String, i: Int): Option[Text.Offset] =
-    if (0 <= i && i <= text.length) Some(i) else None
-
-  val encodings: List[(String, Length)] =
-    List(
-      "UTF-16" -> Length,
-      "UTF-8" -> UTF8.Length,
-      "codepoints" -> Codepoint.Length,
-      "symbols" -> Symbol.Length)
-
-  def encoding(name: String): Length =
-    encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
-      error("Bad text length encoding: " + quote(name) +
-        " (expected " + commas_quote(encodings.map(_._1)) + ")")
-}
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/General/symbol.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -130,11 +130,11 @@
 
   def length(text: CharSequence): Int = iterator(text).length
 
-  object Length extends isabelle.Length
+  object Length extends Text.Length
   {
     def apply(text: String): Int = length(text)
     def offset(text: String, i: Int): Option[Text.Offset] =
-      if (i <= 0 || iterator(text).forall(s => s.length == 1)) isabelle.Length.offset(text, i)
+      if (i <= 0 || iterator(text).forall(s => s.length == 1)) Text.Length.offset(text, i)
       else if (i <= length(text)) Some(iterator(text).take(i).mkString.length)
       else None
   }
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -275,7 +275,7 @@
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
   | Comment => (Markup.comment, "")
-  | Error msg => (Markup.bad, msg)
+  | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/ML/ml_lex.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -147,7 +147,7 @@
   | Char => (Markup.ML_char, "")
   | String => (if SML then Markup.SML_string else Markup.ML_string, "")
   | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
-  | Error msg => (Markup.bad, msg)
+  | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 in
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -116,7 +116,7 @@
       Input.source_explode (Token.input_of tok)
       |> map_filter (fn (sym, pos) =>
           if Symbol.is_malformed sym
-          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
+          then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
     val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
@@ -242,7 +242,7 @@
         let
           val _ = status tr Markup.failed;
           val _ = status tr Markup.finished;
-          val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
+          val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else ();
         in {failed = true, command = tr, state = st} end
     | SOME st' =>
         let
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -808,7 +808,7 @@
               node.commands.iterator.takeWhile(_ != command).map(_.source) ++
                 (if (offset == 0) Iterator.empty
                  else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Text.Length))
             Line.Node_Position(name, pos)
           }
 
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/execution.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -116,7 +116,7 @@
                   Exn.Exn exn =>
                    (status task [Markup.failed];
                     status task [Markup.finished];
-                    Output.report [Markup.markup_only Markup.bad];
+                    Output.report [Markup.markup_only (Markup.bad ())];
                     if exec_id = 0 then ()
                     else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
                 | Exn.Res _ =>
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -31,12 +31,12 @@
         case i => i
       }
 
-    def advance(text: String, length: Length = Length): Position =
+    def advance(text: String, text_length: Text.Length): Position =
       if (text.isEmpty) this
       else {
         val lines = Library.split_lines(text)
         val l = line + lines.length - 1
-        val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last))
+        val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last))
         Position(l, c)
       }
   }
@@ -80,21 +80,14 @@
 
   object Document
   {
-    val empty: Document = new Document(Nil)
-
-    def apply(lines: List[Line]): Document =
-      if (lines.isEmpty) empty
-      else new Document(lines)
-
-    def apply(text: String): Document =
-      if (text == "") empty
-      else if (text.contains('\r'))
-        new Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))))
+    def apply(text: String, text_length: Text.Length): Document =
+      if (text.contains('\r'))
+        Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))), text_length)
       else
-        new Document(Library.split_lines(text).map(s => Line(s)))
+        Document(Library.split_lines(text).map(s => Line(s)), text_length)
   }
 
-  final class Document private(val lines: List[Line])
+  sealed case class Document(lines: List[Line], text_length: Text.Length)
   {
     def make_text: String = lines.mkString("", "\n", "")
 
@@ -107,7 +100,7 @@
       }
     override def hashCode(): Int = lines.hashCode
 
-    def position(offset: Text.Offset, length: Length = Length): Position =
+    def position(text_offset: Text.Offset): Position =
     {
       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
       {
@@ -116,25 +109,34 @@
           case line :: ls =>
             val n = line.text.length
             if (ls.isEmpty || i <= n)
-              Position(lines_count).advance(line.text.substring(n - i), length)
+              Position(lines_count).advance(line.text.substring(n - i), text_length)
             else move(i - (n + 1), lines_count + 1, ls)
         }
       }
-      move(offset, 0, lines)
+      move(text_offset, 0, lines)
     }
 
-    def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
+    def range(text_range: Text.Range): Range =
+      Range(position(text_range.start), position(text_range.stop))
+
+    def offset(pos: Position): Option[Text.Offset] =
     {
       val l = pos.line
       val c = pos.column
       if (0 <= l && l < lines.length) {
         val line_offset =
           if (l == 0) 0
-          else (0 /: lines.iterator.take(l - 1))({ case (n, line) => n + length(line.text) + 1 })
-        length.offset(lines(l).text, c).map(line_offset + _)
+          else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 }
+        text_length.offset(lines(l).text, c).map(line_offset + _)
       }
       else None
     }
+
+    lazy val end_offset: Text.Offset =
+      if (lines.isEmpty) 0
+      else ((0 /: lines) { case (n, line) => n + text_length(line.text) + 1 }) - 1
+
+    def full_range: Text.Range = Text.Range(0, end_offset)
   }
 
 
@@ -148,8 +150,6 @@
 {
   require(text.forall(c => c != '\r' && c != '\n'))
 
-  lazy val length_codepoints: Int = Codepoint.iterator(text).length
-
   override def equals(that: Any): Boolean =
     that match {
       case other: Line => text == other.text
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -173,7 +173,7 @@
   val protocolN: string
   val reportN: string val report: T
   val no_reportN: string val no_report: T
-  val badN: string val bad: T
+  val badN: string val bad: unit -> T
   val intensifyN: string val intensify: T
   val browserN: string
   val graphviewN: string
@@ -573,7 +573,8 @@
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
-val (badN, bad) = markup_elem "bad";
+val badN = "bad";
+fun bad () = (badN, serial_properties (serial ()));
 
 val (intensifyN, intensify) = markup_elem "intensify";
 
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -10,6 +10,35 @@
 
 object Rendering
 {
+  /* message priorities */
+
+  val state_pri = 1
+  val writeln_pri = 2
+  val information_pri = 3
+  val tracing_pri = 4
+  val warning_pri = 5
+  val legacy_pri = 6
+  val error_pri = 7
+
+  val message_pri = Map(
+    Markup.STATE -> state_pri,
+    Markup.STATE_MESSAGE -> state_pri,
+    Markup.WRITELN -> writeln_pri,
+    Markup.WRITELN_MESSAGE -> writeln_pri,
+    Markup.INFORMATION -> information_pri,
+    Markup.INFORMATION_MESSAGE -> information_pri,
+    Markup.TRACING -> tracing_pri,
+    Markup.TRACING_MESSAGE -> tracing_pri,
+    Markup.WARNING -> warning_pri,
+    Markup.WARNING_MESSAGE -> warning_pri,
+    Markup.LEGACY -> legacy_pri,
+    Markup.LEGACY_MESSAGE -> legacy_pri,
+    Markup.ERROR -> error_pri,
+    Markup.ERROR_MESSAGE -> error_pri)
+
+
+  /* markup elements */
+
   private val tooltip_descriptions =
     Map(
       Markup.CITATION -> "citation",
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/text.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -25,6 +25,7 @@
   {
     def apply(start: Offset): Range = Range(start, start)
 
+    val full: Range = apply(0, Integer.MAX_VALUE / 2)
     val offside: Range = apply(-1)
 
     object Ordering extends scala.math.Ordering[Text.Range]
@@ -79,7 +80,7 @@
   {
     val empty: Perspective = Perspective(Nil)
 
-    def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2)))
+    def full: Perspective = Perspective(List(Range.full))
 
     def apply(ranges: Seq[Range]): Perspective =
     {
@@ -180,4 +181,32 @@
         (rest, remove(i, count, string))
       }
   }
+
+
+  /* text length wrt. encoding */
+
+  trait Length
+  {
+    def apply(text: String): Int
+    def offset(text: String, i: Int): Option[Text.Offset]
+  }
+
+  object Length extends Length
+  {
+    def apply(text: String): Int = text.length
+    def offset(text: String, i: Int): Option[Text.Offset] =
+      if (0 <= i && i <= text.length) Some(i) else None
+
+    val encodings: List[(String, Length)] =
+      List(
+        "UTF-16" -> Length,
+        "UTF-8" -> UTF8.Length,
+        "codepoints" -> Codepoint.Length,
+        "symbols" -> Symbol.Length)
+
+    def encoding(name: String): Length =
+      encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
+        error("Bad text length encoding: " + quote(name) +
+          " (expected " + commas_quote(encodings.map(_._1)) + ")")
+  }
 }
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Pure.thy	Wed Dec 28 20:42:28 2016 +0100
@@ -991,7 +991,7 @@
 local
 
 fun report_back () =
-  Output.report [Markup.markup Markup.bad "Explicit backtracking"];
+  Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
 
 val _ =
   Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -217,7 +217,7 @@
   (case xsym of
     Delim s =>
       if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then
-        [((pos, Markup.bad),
+        [((pos, Markup.bad ()),
           "Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")]
       else []
   | _ => []);
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -375,7 +375,7 @@
 
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
-    Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
+    Markup.markup_report (Context_Position.reported_text ctxt pos (Markup.bad ()) ""));
 
 fun parse_sort ctxt =
   Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
@@ -746,7 +746,7 @@
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
       | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
-      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
+      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x))
       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Tools/print_operation.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -49,7 +49,7 @@
     (fn {state, args, writeln_result, ...} =>
       let
         val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
-        fun err s = Pretty.mark_str (Markup.bad, s);
+        fun err s = Pretty.mark_str (Markup.bad (), s);
         fun print name =
           (case AList.lookup (op =) (Synchronized.value print_operations) name of
             SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/build-jars	Wed Dec 28 20:42:28 2016 +0100
@@ -49,7 +49,6 @@
   General/graphics_file.scala
   General/http_server.scala
   General/json.scala
-  General/length.scala
   General/linear_set.scala
   General/logger.scala
   General/long_name.scala
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Pure/skip_proof.ML
--- a/src/Pure/skip_proof.ML	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/skip_proof.ML	Wed Dec 28 20:42:28 2016 +0100
@@ -19,7 +19,7 @@
 
 fun report ctxt =
   if Context_Position.is_visible ctxt then
-    Output.report [Markup.markup Markup.bad "Skipped proof"]
+    Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
   else ();
 
 
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/VSCode/etc/options
--- a/src/Tools/VSCode/etc/options	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/etc/options	Wed Dec 28 20:42:28 2016 +0100
@@ -1,7 +1,16 @@
 (* :mode=isabelle-options: *)
 
+option vscode_input_delay : real = 0.3
+  -- "delay for client input (edits)"
+
+option vscode_output_delay : real = 0.5
+  -- "delay for client output (rendering)"
+
 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)"
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -90,13 +90,20 @@
 
   /* display message */
 
-  def display_message(message_type: Int, message: String, show: Boolean = true): Unit =
-    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(message), show))
+  def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
+    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))
+
+  def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
+  def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
+  def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }
 
-  def error_message(message: String, show: Boolean = true): Unit =
-    display_message(Protocol.MessageType.Error, message, show)
-  def warning(message: String, show: Boolean = true): Unit =
-    display_message(Protocol.MessageType.Warning, message, show)
-  def writeln(message: String, show: Boolean = true): Unit =
-    display_message(Protocol.MessageType.Info, message, show)
+  def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
+  def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
+  def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
+
+
+  /* diagnostics */
+
+  def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
+    write(Protocol.PublishDiagnostics(uri, diagnostics))
 }
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -14,12 +14,20 @@
 
 case class Document_Model(
   session: Session, doc: Line.Document, node_name: Document.Node.Name,
-  changed: Boolean = true)
+  changed: Boolean = true,
+  published_diagnostics: List[Text.Info[Command.Results]] = Nil)
 {
+  override def toString: String = node_name.toString
+
+
+  /* name */
+
+  def uri: String = node_name.node
+  def is_theory: Boolean = node_name.is_theory
+
+
   /* header */
 
-  def is_theory: Boolean = node_name.is_theory
-
   def node_header(resources: VSCode_Resources): Document.Node.Header =
     resources.special_header(node_name) getOrElse
     {
@@ -48,10 +56,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)
 }
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -311,4 +311,32 @@
     def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
       ResponseMessage(id, Some(result.map(Location.apply(_))))
   }
+
+
+  /* diagnostics */
+
+  sealed case class Diagnostic(range: Line.Range, message: String,
+    severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
+  {
+    def json: JSON.T =
+      Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
+      (severity match { case Some(x) => Map("severity" -> x) case None => Map.empty }) ++
+      (code match { case Some(x) => Map("code" -> x) case None => Map.empty }) ++
+      (source match { case Some(x) => Map("source" -> x) case None => Map.empty })
+  }
+
+  object DiagnosticSeverity
+  {
+    val Error = 0
+    val Warning = 1
+    val Information = 2
+    val Hint = 3
+  }
+
+  object PublishDiagnostics
+  {
+    def apply(uri: String, diagnostics: List[Diagnostic]): JSON.T =
+      Notification("textDocument/publishDiagnostics",
+        Map("uri" -> uri, "diagnostics" -> diagnostics.map(_.json)))
+  }
 }
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -27,14 +27,14 @@
   {
     try {
       var log_file: Option[Path] = None
-      var text_length = Length.encoding(default_text_length)
+      var text_length = Text.Length.encoding(default_text_length)
       var dirs: List[Path] = Nil
       var logic = default_logic
       var modes: List[String] = Nil
       var options = Options.init()
 
       def text_length_choice: String =
-        commas(Length.encodings.map(
+        commas(Text.Length.encodings.map(
           { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
 
       val getopts = Getopts("""
@@ -51,7 +51,7 @@
   Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
 """,
         "L:" -> (arg => log_file = Some(Path.explode(arg))),
-        "T:" -> (arg => Length.encoding(arg)),
+        "T:" -> (arg => Text.Length.encoding(arg)),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "l:" -> (arg => logic = arg),
         "m:" -> (arg => modes = arg :: modes),
@@ -88,13 +88,15 @@
 
   sealed case class State(
     session: Option[Session] = None,
-    models: Map[String, Document_Model] = Map.empty)
+    models: Map[String, Document_Model] = Map.empty,
+    pending_input: Set[Document.Node.Name] = Set.empty,
+    pending_output: Set[Document.Node.Name] = Set.empty)
 }
 
 class Server(
   channel: Channel,
   options: Options,
-  text_length: Length = Length.encoding(Server.default_text_length),
+  text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
   session_name: String = Server.default_logic,
   session_dirs: List[Path] = Nil,
   modes: List[String] = Nil)
@@ -109,11 +111,88 @@
   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)
-      offset <- model.doc.offset(node_pos.pos, text_length)
+      rendering = model.rendering(options)
+      offset <- model.doc.offset(node_pos.pos)
     } yield (rendering, offset)
 
 
+  /* input from client */
+
+  private val delay_input =
+    Standard_Thread.delay_last(options.seconds("vscode_input_delay")) {
+      state.change(st =>
+        {
+          val changed =
+            (for {
+              node_name <- st.pending_input.iterator
+              model <- st.models.get(node_name.node)
+              if model.changed } yield model).toList
+          session.update(Document.Blobs.empty,
+            for { model <- changed; edit <- model.node_edits(resources) } yield edit)
+          st.copy(
+            models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
+            pending_input = Set.empty)
+        })
+    }
+
+  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, text_length), node_name)
+        st.copy(
+          models = st.models + (uri -> model),
+          pending_input = st.pending_input + node_name)
+      })
+    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 =
+    Standard_Thread.delay_last(options.seconds("vscode_output_delay")) {
+      if (session.current_state().stable_tip_version.isEmpty) delay_output.invoke()
+      else {
+        state.change(st =>
+          {
+            val changed_iterator =
+              for {
+                node_name <- st.pending_output.iterator
+                model <- st.models.get(node_name.node)
+                rendering = model.rendering(options)
+                (diagnostics, model1) <- model.publish_diagnostics(rendering)
+              } yield {
+                channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
+                model1
+              }
+            st.copy(
+              models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
+              pending_output = Set.empty)
+          }
+        )
+      }
+    }
+
+
+  /* syslog */
+
+  private val all_messages =
+    Session.Consumer[Prover.Message](getClass.getName) {
+      case output: Prover.Output if output.is_syslog =>
+        channel.log_writeln(XML.content(output.message))
+      case _ =>
+    }
+
+
   /* init and exit */
 
   def init(id: Protocol.Id)
@@ -156,6 +235,9 @@
         }
       session.phase_changed += session_phase
 
+      session.commands_changed += commands_changed
+      session.all_messages += all_messages
+
       session.start(receiver =>
         Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
           modes = modes, receiver = receiver))
@@ -177,11 +259,15 @@
             Session.Consumer(getClass.getName) {
               case Session.Inactive =>
                 session.phase_changed -= session_phase
+                session.commands_changed -= commands_changed
+                session.all_messages -= all_messages
                 reply("")
               case _ =>
             }
           session.phase_changed += session_phase
           session.stop()
+          delay_input.revoke()
+          delay_output.revoke()
           st.copy(session = None)
       })
   }
@@ -192,35 +278,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 +288,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)
         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))
   }
@@ -275,7 +331,7 @@
           case _ => channel.log("### IGNORED")
         }
       }
-      catch { case exn: Throwable => channel.error_message(Exn.message(exn)) }
+      catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
     }
 
     @tailrec def loop()
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 20:42:28 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](
+      model.doc.full_range, 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)
+      (_, 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")
@@ -44,9 +89,8 @@
         opt_text match {
           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)
-            Line.Range(position(range.start), position(range.stop))
+            val doc = Line.Document(text, model.doc.text_length)
+            doc.range(chunk.decode(range))
           case _ =>
             Line.Range(Line.Position((line1 - 1) max 0))
         })
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -69,6 +69,9 @@
 
 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
 {
+  override def toString: String = node_name.toString
+
+
   /* header */
 
   def is_theory: Boolean = node_name.is_theory
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -270,7 +270,8 @@
             JEdit_Lib.buffer_lock(buffer) {
               (Line.Position.zero /:
                 (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
-                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
+                  zipWithIndex.takeWhile(p => p._2 < offset - 1).
+                  map(_._1)))(_.advance(_, Text.Length))
             }
           hyperlink_file(focus, Line.Node_Position(name, pos))
         case _ =>
diff -r ef0a5fd30f3b -r 1d645e6efd89 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 28 20:42:28 2016 +0100
@@ -25,33 +25,6 @@
     new JEdit_Rendering(snapshot, options)
 
 
-  /* message priorities */
-
-  private val state_pri = 1
-  private val writeln_pri = 2
-  private val information_pri = 3
-  private val tracing_pri = 4
-  private val warning_pri = 5
-  private val legacy_pri = 6
-  private val error_pri = 7
-
-  private val message_pri = Map(
-    Markup.STATE -> state_pri,
-    Markup.STATE_MESSAGE -> state_pri,
-    Markup.WRITELN -> writeln_pri,
-    Markup.WRITELN_MESSAGE -> writeln_pri,
-    Markup.INFORMATION -> information_pri,
-    Markup.INFORMATION_MESSAGE -> information_pri,
-    Markup.TRACING -> tracing_pri,
-    Markup.TRACING_MESSAGE -> tracing_pri,
-    Markup.WARNING -> warning_pri,
-    Markup.WARNING_MESSAGE -> warning_pri,
-    Markup.LEGACY -> legacy_pri,
-    Markup.LEGACY_MESSAGE -> legacy_pri,
-    Markup.ERROR -> error_pri,
-    Markup.ERROR_MESSAGE -> error_pri)
-
-
   /* popup window bounds */
 
   def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
@@ -529,13 +502,9 @@
       snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
         range, Nil, JEdit_Rendering.tooltip_message_elements, _ =>
         {
-          case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
+          case (msgs, Text.Info(info_range,
+            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
           if body.nonEmpty =>
-            val entry: Command.Results.Entry = (Document_ID.make(), msg)
-            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
-
-          case (msgs, Text.Info(info_range,
-            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) =>
             val entry: Command.Results.Entry =
               serial -> XML.Elem(Markup(Markup.message(name), props), body)
             Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
@@ -563,20 +532,20 @@
   /* gutter */
 
   private def gutter_message_pri(msg: XML.Tree): Int =
-    if (Protocol.is_error(msg)) JEdit_Rendering.error_pri
-    else if (Protocol.is_legacy(msg)) JEdit_Rendering.legacy_pri
-    else if (Protocol.is_warning(msg)) JEdit_Rendering.warning_pri
-    else if (Protocol.is_information(msg)) JEdit_Rendering.information_pri
+    if (Protocol.is_error(msg)) Rendering.error_pri
+    else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
+    else if (Protocol.is_warning(msg)) Rendering.warning_pri
+    else if (Protocol.is_information(msg)) Rendering.information_pri
     else 0
 
   private lazy val gutter_message_content = Map(
-    JEdit_Rendering.information_pri ->
+    Rendering.information_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_information_icon")), information_message_color),
-    JEdit_Rendering.warning_pri ->
+    Rendering.warning_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), warning_message_color),
-    JEdit_Rendering.legacy_pri ->
+    Rendering.legacy_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), warning_message_color),
-    JEdit_Rendering.error_pri ->
+    Rendering.error_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_error_icon")), error_message_color))
 
   def gutter_content(range: Text.Range): Option[(Icon, Color)] =
@@ -596,18 +565,18 @@
   /* squiggly underline */
 
   private lazy val squiggly_colors = Map(
-    JEdit_Rendering.writeln_pri -> writeln_color,
-    JEdit_Rendering.information_pri -> information_color,
-    JEdit_Rendering.warning_pri -> warning_color,
-    JEdit_Rendering.legacy_pri -> legacy_color,
-    JEdit_Rendering.error_pri -> error_color)
+    Rendering.writeln_pri -> writeln_color,
+    Rendering.information_pri -> information_color,
+    Rendering.warning_pri -> warning_color,
+    Rendering.legacy_pri -> legacy_color,
+    Rendering.error_pri -> error_color)
 
   def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   {
     val results =
       snapshot.cumulate[Int](range, 0, JEdit_Rendering.squiggly_elements, _ =>
         {
-          case (pri, Text.Info(_, elem)) => Some(pri max JEdit_Rendering.message_pri(elem.name))
+          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
         })
     for {
       Text.Info(r, pri) <- results
@@ -619,19 +588,19 @@
   /* message output */
 
   private lazy val message_colors = Map(
-    JEdit_Rendering.writeln_pri -> writeln_message_color,
-    JEdit_Rendering.information_pri -> information_message_color,
-    JEdit_Rendering.tracing_pri -> tracing_message_color,
-    JEdit_Rendering.warning_pri -> warning_message_color,
-    JEdit_Rendering.legacy_pri -> legacy_message_color,
-    JEdit_Rendering.error_pri -> error_message_color)
+    Rendering.writeln_pri -> writeln_message_color,
+    Rendering.information_pri -> information_message_color,
+    Rendering.tracing_pri -> tracing_message_color,
+    Rendering.warning_pri -> warning_message_color,
+    Rendering.legacy_pri -> legacy_message_color,
+    Rendering.error_pri -> error_message_color)
 
   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
     val results =
       snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
         {
-          case (pri, Text.Info(_, elem)) => Some(pri max JEdit_Rendering.message_pri(elem.name))
+          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }