incremental document changes;

--- a/src/Tools/VSCode/src/document_model.scala	Thu Mar 09 15:08:44 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Thu Mar 09 15:19:24 2017 +0100
@@ -102,16 +102,25 @@
 
   /* edits */
 
-  def update_text(text: String): Option[Document_Model] =
+  def change_text(text: String, range: Option[Line.Range] = None): Option[Document_Model] =
   {
-    val old_text = content.text
-    val new_text = Line.normalize(text)
-    Text.Edit.replace(0, old_text, new_text) match {
-      case Nil => None
-      case edits =>
-        val content1 = Document_Model.Content(Line.Document(new_text, content.doc.text_length))
-        val pending_edits1 = pending_edits ::: edits
-        Some(copy(content = content1, pending_edits = pending_edits1))
+    val insert = Line.normalize(text)
+    range match {
+      case None =>
+        Text.Edit.replace(0, content.text, insert) match {
+          case Nil => None
+          case edits =>
+            val content1 = Document_Model.Content(Line.Document(insert, content.doc.text_length))
+            Some(copy(content = content1, pending_edits = pending_edits ::: edits))
+        }
+      case Some(remove) =>
+        content.doc.change(remove, insert) match {
+          case None => error("Failed to apply document change: " + remove)
+          case Some((Nil, _)) => None
+          case Some((edits, doc1)) =>
+            val content1 = Document_Model.Content(doc1)
+            Some(copy(content = content1, pending_edits = pending_edits ::: edits))
+        }
     }
   }
 

--- a/src/Tools/VSCode/src/protocol.scala	Thu Mar 09 15:08:44 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Thu Mar 09 15:19:24 2017 +0100
@@ -10,7 +10,6 @@
 
 import isabelle._
 
-
 import java.io.{File => JFile}
 
 
@@ -138,7 +137,7 @@
   {
     val json: JSON.T =
       Map(
-        "textDocumentSync" -> 1,
+        "textDocumentSync" -> 2,
         "completionProvider" -> Map("resolveProvider" -> false, "triggerCharacters" -> Nil),
         "hoverProvider" -> true,
         "definitionProvider" -> true,
@@ -260,34 +259,22 @@
   }
 
 
-  sealed abstract class TextDocumentContentChange
-  case class TextDocumentContent(text: String) extends TextDocumentContentChange
-  case class TextDocumentChange(range: Line.Range, range_length: Int, text: String)
-    extends TextDocumentContentChange
-
-  object TextDocumentContentChange
-  {
-    def unapply(json: JSON.T): Option[TextDocumentContentChange] =
-      for { text <- JSON.string(json, "text") }
-      yield {
-        (JSON.value(json, "range"), JSON.int(json, "rangeLength")) match {
-          case (Some(Range(range)), Some(range_length)) =>
-            TextDocumentChange(range, range_length, text)
-          case _ => TextDocumentContent(text)
-        }
-      }
-  }
+  sealed case class TextDocumentChange(range: Option[Line.Range], text: String)
 
   object DidChangeTextDocument
   {
-    def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentContentChange])] =
+    def unapply_change(json: JSON.T): Option[TextDocumentChange] =
+      for { text <- JSON.string(json, "text") }
+      yield TextDocumentChange(JSON.value(json, "range", Range.unapply _), text)
+
+    def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentChange])] =
       json match {
         case Notification("textDocument/didChange", Some(params)) =>
           for {
             doc <- JSON.value(params, "textDocument")
             uri <- JSON.string(doc, "uri")
             version <- JSON.long(doc, "version")
-            changes <- JSON.array(params, "contentChanges", TextDocumentContentChange.unapply _)
+            changes <- JSON.array(params, "contentChanges", unapply_change _)
           } yield (Url.canonical_file(uri), version, changes)
         case _ => None
       }

--- a/src/Tools/VSCode/src/server.scala	Thu Mar 09 15:08:44 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Thu Mar 09 15:19:24 2017 +0100
@@ -1,9 +1,11 @@
 /*  Title:      Tools/VSCode/src/server.scala
     Author:     Makarius
 
-Server for VS Code Language Server Protocol 2.0, see also
+Server for VS Code Language Server Protocol 2.0/3.0, see also
 https://github.com/Microsoft/language-server-protocol
 https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
+
+PIDE protocol extensions depend on system option "vscode_pide_extensions".
 */
 
 package isabelle.vscode
@@ -143,7 +145,14 @@
 
   private def update_document(file: JFile, text: String)
   {
-    resources.update_model(session, file, text)
+    resources.change_model(session, file, text)
+    delay_input.invoke()
+    delay_output.invoke()
+  }
+
+  private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
+  {
+    changes.foreach(change => resources.change_model(session, file, change.text, change.range))
     delay_input.invoke()
     delay_output.invoke()
   }
@@ -351,12 +360,9 @@
           case Protocol.Initialize(id) => init(id)
           case Protocol.Shutdown(id) => shutdown(id)
           case Protocol.Exit(()) => exit()
-          case Protocol.DidOpenTextDocument(file, lang, version, text) =>
-            update_document(file, text)
-          case Protocol.DidChangeTextDocument(file, version, List(Protocol.TextDocumentContent(text))) =>
-            update_document(file, text)
-          case Protocol.DidCloseTextDocument(file) =>
-            close_document(file)
+          case Protocol.DidOpenTextDocument(file, _, _, text) => update_document(file, text)
+          case Protocol.DidChangeTextDocument(file, _, changes) => change_document(file, changes)
+          case Protocol.DidCloseTextDocument(file) => close_document(file)
           case Protocol.Completion(id, node_pos) => completion(id, node_pos)
           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)

--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Mar 09 15:08:44 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Mar 09 15:19:24 2017 +0100
@@ -122,12 +122,12 @@
       case None => false
     }
 
-  def update_model(session: Session, file: JFile, text: String)
+  def change_model(session: Session, file: JFile, text: String, range: Option[Line.Range] = None)
   {
     state.change(st =>
       {
         val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
-        val model1 = (model.update_text(text) getOrElse model).external(false)
+        val model1 = (model.change_text(text, range) getOrElse model).external(false)
         st.update_models(Some(file -> model1))
       })
   }
@@ -147,7 +147,7 @@
             (file, model) <- st.models.iterator
             if changed_files(file) && model.external_file
             text <- read_file_content(file)
-            model1 <- model.update_text(text)
+            model1 <- model.change_text(text)
           } yield (file, model1)).toList
         st.update_models(changed_models)
       })
@@ -193,7 +193,7 @@
           }
           yield {
             val model = Document_Model.init(session, node_name)
-            val model1 = (model.update_text(text) getOrElse model).external(true)
+            val model1 = (model.change_text(text) getOrElse model).external(true)
             (file, model1)
           }).toList