# HG changeset patch # User wenzelm # Date 1483625751 -3600 # Node ID 415dafeb966939fb1fefdb8d30612c2c6674d490 # Parent c0c648911f1aa2d83c6418b00b8fbe55964b573e manage document blobs as well; diff -r c0c648911f1a -r 415dafeb9669 src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Thu Jan 05 12:23:25 2017 +0100 +++ b/src/Pure/PIDE/line.scala Thu Jan 05 15:15:51 2017 +0100 @@ -136,6 +136,12 @@ else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1 def full_range: Text.Range = Text.Range(0, length) + + lazy val blob: (Bytes, Symbol.Text_Chunk) = + { + val text = make_text + (Bytes(text), Symbol.Text_Chunk(text)) + } } diff -r c0c648911f1a -r 415dafeb9669 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Thu Jan 05 12:23:25 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Thu Jan 05 15:15:51 2017 +0100 @@ -45,6 +45,8 @@ def external(b: Boolean): Document_Model = copy(external_file = b) + def node_visible: Boolean = !external_file + /* header */ @@ -60,13 +62,32 @@ /* perspective */ - def node_visible: Boolean = !external_file + def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = + { + if (is_theory) { + val snapshot = this.snapshot() + + val text_perspective = + if (node_visible || snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty) + Text.Perspective.full + else Text.Perspective.empty - def text_perspective: Text.Perspective = - if (node_visible) Text.Perspective.full else Text.Perspective.empty + (snapshot.node.load_commands_changed(doc_blobs), + Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)) + } + else (false, Document.Node.no_perspective_text) + } + - def node_perspective: Document.Node.Perspective_Text = - Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty) + /* blob */ + + def get_blob: Option[Document.Blob] = + if (is_theory) None + else { + val (bytes, chunk) = doc.blob + val changed = pending_edits.nonEmpty + Some((Document.Blob(bytes, chunk, changed))) + } /* edits */ @@ -84,17 +105,20 @@ } } - def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] = + def flush_edits(doc_blobs: Document.Blobs): Option[(List[Document.Edit_Text], Document_Model)] = { - val perspective = node_perspective - if (pending_edits.nonEmpty || last_perspective != perspective) { - val text_edits = pending_edits.toList - val edits = - session.header_edit(node_name, node_header) :: - (if (text_edits.isEmpty) Nil - else List[Document.Edit_Text](node_name -> Document.Node.Edits(text_edits))) ::: - (if (last_perspective == perspective) Nil - else List[Document.Edit_Text](node_name -> perspective)) + val (reparse, perspective) = node_perspective(doc_blobs) + if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { + val edits: List[Document.Edit_Text] = + get_blob match { + case None => + List(session.header_edit(node_name, node_header), + node_name -> Document.Node.Edits(pending_edits.toList), + node_name -> perspective) + case Some(blob) => + List(node_name -> Document.Node.Blob(blob), + node_name -> Document.Node.Edits(pending_edits.toList)) + } Some((edits, copy(pending_edits = Vector.empty, last_perspective = perspective))) } else None diff -r c0c648911f1a -r 415dafeb9669 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Thu Jan 05 12:23:25 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Thu Jan 05 15:15:51 2017 +0100 @@ -110,13 +110,16 @@ /* input from client or file-system */ - private val delay_input = + private val delay_input: Standard_Thread.Delay = Standard_Thread.delay_last(options.seconds("vscode_input_delay")) { resources.flush_input(session) } - private val delay_load = - Standard_Thread.delay_last(options.seconds("vscode_load_delay")) - { if (resources.resolve_dependencies(session, watcher)) delay_input.invoke() } + private val delay_load: Standard_Thread.Delay = + Standard_Thread.delay_last(options.seconds("vscode_load_delay")) { + val (invoke_input, invoke_load) = resources.resolve_dependencies(session, watcher) + if (invoke_input) delay_input.invoke() + if (invoke_load) delay_load.invoke + } private val watcher = File_Watcher(sync_documents(_), options.seconds("vscode_load_delay")) @@ -201,7 +204,8 @@ new VSCode_Resources(options, text_length, content.loaded_theories, content.known_theories, content.syntax, log) { override def commit(change: Session.Change): Unit = - if (change.deps_changed) delay_load.invoke() + if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) + delay_load.invoke() } Some(new Session(resources) { diff -r c0c648911f1a -r 415dafeb9669 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Thu Jan 05 12:23:25 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Jan 05 15:15:51 2017 +0100 @@ -22,6 +22,14 @@ models: Map[JFile, Document_Model] = Map.empty, pending_input: Set[JFile] = Set.empty, pending_output: Set[JFile] = Set.empty) + { + lazy val document_blobs: Document.Blobs = + Document.Blobs( + (for { + (_, model) <- models.iterator + blob <- model.get_blob + } yield (model.node_name -> blob)).toMap) + } } class VSCode_Resources( @@ -79,6 +87,12 @@ def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file) def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name)) + def visible_node(name: Document.Node.Name): Boolean = + get_model(name) match { + case Some(model) => model.node_visible + case None => false + } + def update_model(session: Session, file: JFile, text: String) { state.change(st => @@ -134,33 +148,55 @@ val thy_info = new Thy_Info(this) - def resolve_dependencies(session: Session, watcher: File_Watcher): Boolean = + def resolve_dependencies(session: Session, watcher: File_Watcher): (Boolean, Boolean) = { state.change_result(st => { + /* theory files */ + val thys = (for ((_, model) <- st.models.iterator if model.is_theory) yield (model.node_name, Position.none)).toList + val thy_files = thy_info.dependencies("", thys).deps.map(_.name) + + + /* auxiliary files */ + + val stable_tip_version = + if (st.models.forall({ case (_, model) => model.pending_edits.isEmpty })) + session.current_state().stable_tip_version + else None + + val aux_files = + stable_tip_version match { + case Some(version) => undefined_blobs(version.nodes) + case None => Nil + } + + + /* loaded models */ + val loaded_models = (for { - dep <- thy_info.dependencies("", thys).deps.iterator - file = node_file(dep.name) + node_name <- thy_files.iterator ++ aux_files.iterator + file = node_file(node_name) if !st.models.isDefinedAt(file) text <- { watcher.register_parent(file); try_read(file) } } yield { - val model = Document_Model.init(session, node_name(file)) + val model = Document_Model.init(session, node_name) val model1 = (model.update_text(text) getOrElse model).external(true) (file, model1) }).toList - if (loaded_models.isEmpty) (false, st) - else - (true, - st.copy( - models = st.models ++ loaded_models, - pending_input = st.pending_input ++ loaded_models.iterator.map(_._1))) + val invoke_input = loaded_models.nonEmpty + val invoke_load = stable_tip_version.isEmpty + + ((invoke_input, invoke_load), + st.copy( + models = st.models ++ loaded_models, + pending_input = st.pending_input ++ loaded_models.iterator.map(_._1))) }) } @@ -175,10 +211,10 @@ (for { file <- st.pending_input.iterator model <- st.models.get(file) - (edits, model1) <- model.flush_edits + (edits, model1) <- model.flush_edits(st.document_blobs) } yield (edits, (file, model1))).toList - session.update(Document.Blobs.empty, changed_models.flatMap(_._1)) + session.update(st.document_blobs, changed_models.flatMap(_._1)) st.copy( models = (st.models /: changed_models.iterator.map(_._2))(_ + _), pending_input = Set.empty)