# HG changeset patch # User wenzelm # Date 1495740022 -7200 # Node ID 0f7821a07aa99cc8de7f090d4a395ce983660a18 # Parent 4a1b666b6362f839048d18b1f1ab7a7dc45bf5f8 restricted perspective depending on the caret -- important for reactivity when editing big files; diff -r 4a1b666b6362 -r 0f7821a07aa9 src/Tools/VSCode/etc/options --- 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)" diff -r 4a1b666b6362 -r 0f7821a07aa9 src/Tools/VSCode/src/document_model.scala --- 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))) diff -r 4a1b666b6362 -r 0f7821a07aa9 src/Tools/VSCode/src/server.scala --- 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() } diff -r 4a1b666b6362 -r 0f7821a07aa9 src/Tools/VSCode/src/vscode_resources.scala --- 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)] = {