restricted perspective depending on the caret -- important for reactivity when editing big files;

--- a/src/Tools/VSCode/etc/options	Thu May 25 19:50:37 2017 +0200
+++ b/src/Tools/VSCode/etc/options	Thu May 25 21:20:22 2017 +0200
@@ -23,3 +23,6 @@
 
 option vscode_unicode_symbols : bool = false
   -- "output Isabelle symbols via Unicode (according to etc/symbols)"
+
+option vscode_caret_perspective : int = 50
+  -- "number of visible lines above and below the caret (0: unrestricted)"

--- a/src/Tools/VSCode/src/document_model.scala	Thu May 25 19:50:37 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Thu May 25 21:20:22 2017 +0200
@@ -79,15 +79,35 @@
 
   /* perspective */
 
-  def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
+  def node_perspective(doc_blobs: Document.Blobs, caret: Option[Line.Position])
+    : (Boolean, Document.Node.Perspective_Text) =
   {
     if (is_theory) {
       val snapshot = this.snapshot()
 
+      val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
+      val caret_range =
+        if (caret_perspective != 0) {
+          caret match {
+            case Some(pos) =>
+              val doc = content.doc
+              val pos1 = Line.Position((pos.line - caret_perspective) max 0)
+              val pos2 = Line.Position((pos.line + caret_perspective + 1) min doc.lines.length)
+              Text.Range(doc.offset(pos1).get, doc.offset(pos2).get)
+            case None => Text.Range.offside
+          }
+        }
+        else if (node_visible) content.text_range
+        else Text.Range.offside
+
       val text_perspective =
-        if (node_visible || snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty)
+        if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty)
           Text.Perspective.full
-        else Text.Perspective.empty
+        else
+          content.text_range.try_restrict(caret_range) match {
+            case Some(range) => Text.Perspective(List(range))
+            case None => Text.Perspective.empty
+          }
 
       (snapshot.node.load_commands_changed(doc_blobs),
         Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty))
@@ -127,9 +147,10 @@
     }
   }
 
-  def flush_edits(doc_blobs: Document.Blobs): Option[(List[Document.Edit_Text], Document_Model)] =
+  def flush_edits(doc_blobs: Document.Blobs, caret: Option[Line.Position])
+    : Option[(List[Document.Edit_Text], Document_Model)] =
   {
-    val (reparse, perspective) = node_perspective(doc_blobs)
+    val (reparse, perspective) = node_perspective(doc_blobs, caret)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
       val edits = node_edits(node_header, pending_edits, perspective)
       Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))

--- a/src/Tools/VSCode/src/server.scala	Thu May 25 19:50:37 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Thu May 25 21:20:22 2017 +0200
@@ -172,6 +172,7 @@
   {
     resources.update_caret(caret)
     delay_caret_update.invoke()
+    delay_input.invoke()
   }
 
 

--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu May 25 19:50:37 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu May 25 21:20:22 2017 +0200
@@ -20,9 +20,9 @@
 
   sealed case class State(
     models: Map[JFile, Document_Model] = Map.empty,
+    caret: Option[(JFile, Line.Position)] = None,
     pending_input: Set[JFile] = Set.empty,
-    pending_output: Set[JFile] = Set.empty,
-    caret: Option[(JFile, Line.Position)] = None)
+    pending_output: Set[JFile] = Set.empty)
   {
     def update_models(changed: Traversable[(JFile, Document_Model)]): State =
       copy(
@@ -30,6 +30,19 @@
         pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
         pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file })
 
+    def update_caret(new_caret: Option[(JFile, Line.Position)]): State =
+      if (caret == new_caret) this
+      else
+        copy(
+          caret = new_caret,
+          pending_input = pending_input ++ caret.map(_._1) ++ new_caret.map(_._1))
+
+    def get_caret(file: JFile): Option[Line.Position] =
+      caret match {
+        case Some((caret_file, caret_pos)) if caret_file == file => Some(caret_pos)
+        case _ => None
+      }
+
     lazy val document_blobs: Document.Blobs =
       Document.Blobs(
         (for {
@@ -219,7 +232,7 @@
           (for {
             file <- st.pending_input.iterator
             model <- st.models.get(file)
-            (edits, model1) <- model.flush_edits(st.document_blobs)
+            (edits, model1) <- model.flush_edits(st.document_blobs, st.get_caret(file))
           } yield (edits, (file, model1))).toList
 
         session.update(st.document_blobs, changed_models.flatMap(_._1))
@@ -287,7 +300,7 @@
   /* caret handling */
 
   def update_caret(caret: Option[(JFile, Line.Position)])
-  { state.change(_.copy(caret = caret)) }
+  { state.change(_.update_caret(caret)) }
 
   def caret_offset(): Option[(Document_Model, Text.Offset)] =
   {