--- a/src/Pure/General/file_watcher.scala Fri Dec 30 15:40:35 2016 +0100
+++ b/src/Pure/General/file_watcher.scala Fri Dec 30 20:43:40 2016 +0100
@@ -99,7 +99,7 @@
/* shutdown */
- def shutdown
+ def shutdown()
{
watcher_thread.interrupt
watcher_thread.join
--- a/src/Tools/VSCode/src/document_model.scala Fri Dec 30 15:40:35 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Fri Dec 30 20:43:40 2016 +0100
@@ -9,12 +9,31 @@
import isabelle._
+import java.io.{File => JFile}
+
import scala.util.parsing.input.CharSequenceReader
-case class Document_Model(
- session: Session, node_name: Document.Node.Name, doc: Line.Document,
- changed: Boolean = true,
+object Document_Model
+{
+ def init(session: Session, uri: String): Document_Model =
+ {
+ val resources = session.resources.asInstanceOf[VSCode_Resources]
+ val node_name = resources.node_name(uri)
+ val doc = Line.Document("", resources.text_length)
+ Document_Model(session, node_name, doc)
+ }
+}
+
+sealed case class Document_Model(
+ session: Session,
+ node_name: Document.Node.Name,
+ doc: Line.Document,
+ external: Boolean = false,
+ node_visible: Boolean = true,
+ node_required: Boolean = false,
+ last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+ pending_edits: Vector[Text.Edit] = Vector.empty,
published_diagnostics: List[Text.Info[Command.Results]] = Nil)
{
/* name */
@@ -25,6 +44,17 @@
def is_theory: Boolean = node_name.is_theory
+ /* external file */
+
+ val file: JFile = VSCode_Resources.canonical_file(uri)
+
+ def register(watcher: File_Watcher)
+ {
+ val dir = file.getParentFile
+ if (dir != null && dir.isDirectory) watcher.register(dir)
+ }
+
+
/* header */
def node_header: Document.Node.Header =
@@ -37,22 +67,52 @@
}
+ /* perspective */
+
+ def text_perspective: Text.Perspective =
+ if (node_visible) Text.Perspective.full else Text.Perspective.empty
+
+ def node_perspective: Document.Node.Perspective_Text =
+ Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
+
+
/* edits */
- def text_edits: List[Text.Edit] =
- if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
+ def update_text(new_text: String): Option[Document_Model] =
+ {
+ val old_text = doc.make_text
+ if (new_text == old_text) None
+ else {
+ val doc1 = Line.Document(new_text, doc.text_length)
+ val pending_edits1 =
+ if (old_text != "") pending_edits :+ Text.Edit.remove(0, old_text) else pending_edits
+ val pending_edits2 = pending_edits1 :+ Text.Edit.insert(0, new_text)
+ Some(copy(doc = doc1, pending_edits = pending_edits2))
+ }
+ }
- def node_edits: List[Document.Edit_Text] =
- if (changed) {
- List(session.header_edit(node_name, node_header),
- node_name -> Document.Node.Clear(),
- node_name -> Document.Node.Edits(text_edits),
- node_name ->
- Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty))
+ def update_file: Option[Document_Model] =
+ if (external) {
+ try { update_text(File.read(file)) }
+ catch { case ERROR(_) => None }
}
- else Nil
+ else None
- def unchanged: Document_Model = if (changed) copy(changed = false) else this
+ def flush_edits: 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))
+ Some((edits, copy(pending_edits = Vector.empty, last_perspective = perspective)))
+ }
+ else None
+ }
/* diagnostics */
@@ -70,7 +130,7 @@
def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
- def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
+ def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList)
def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
}
--- a/src/Tools/VSCode/src/server.scala Fri Dec 30 15:40:35 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala Fri Dec 30 20:43:40 2016 +0100
@@ -11,7 +11,7 @@
import isabelle._
-import java.io.{PrintStream, OutputStream}
+import java.io.{PrintStream, OutputStream, File => JFile}
import scala.annotation.tailrec
@@ -106,26 +106,43 @@
} yield (rendering, offset)
+ /* document content */
+
+ private def update_document(uri: String, text: String)
+ {
+ resources.update_model(session, uri, text)
+ delay_input.invoke()
+ }
+
+ private def close_document(uri: String)
+ {
+ resources.close_model(uri) match {
+ case Some(model) =>
+ model.register(watcher)
+ sync_external(Set(model.file))
+ case None =>
+ }
+ }
+
+ private def sync_external(changed: Set[JFile]): Unit =
+ if (resources.sync_external(changed)) delay_input.invoke()
+
+ private val watcher = File_Watcher(sync_external(_))
+
+
/* input from client */
private val delay_input =
Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
{ resources.flush_input(session) }
- private def update_document(uri: String, text: String)
- {
- val model = Document_Model(session, resources.node_name(uri), Line.Document(text, text_length))
- resources.update_model(model)
- delay_input.invoke()
- }
-
/* output to client */
private val commands_changed =
Session.Consumer[Session.Commands_Changed](getClass.getName) {
case changed if changed.nodes.nonEmpty =>
- resources.update_output(changed.nodes)
+ resources.update_output(changed.nodes.toList.map(_.node))
delay_output.invoke()
case _ =>
}
@@ -138,6 +155,9 @@
}
+ /* file watcher */
+
+
/* syslog */
private val all_messages =
@@ -165,7 +185,7 @@
val content = Build.session_content(options, false, session_dirs, session_name)
val resources =
new VSCode_Resources(
- options, content.loaded_theories, content.known_theories, content.syntax)
+ options, text_length, content.loaded_theories, content.known_theories, content.syntax)
Some(new Session(resources) {
override def output_delay = options.seconds("editor_output_delay")
@@ -222,6 +242,7 @@
session.stop()
delay_input.revoke()
delay_output.revoke()
+ watcher.shutdown()
None
case None =>
reply("Prover inactive")
@@ -281,7 +302,8 @@
update_document(uri, text)
case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
update_document(uri, text)
- case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
+ case Protocol.DidCloseTextDocument(uri) =>
+ close_document(uri)
case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
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_rendering.scala Fri Dec 30 15:40:35 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Dec 30 20:43:40 2016 +0100
@@ -88,7 +88,7 @@
opt_text match {
case Some(text) if range.start > 0 =>
val chunk = Symbol.Text_Chunk(text)
- val doc = Line.Document(text, model.doc.text_length)
+ val doc = Line.Document(text, resources.text_length)
doc.range(chunk.decode(range))
case _ =>
Line.Range(Line.Position((line1 - 1) max 0))
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 30 15:40:35 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 30 20:43:40 2016 +0100
@@ -29,12 +29,13 @@
sealed case class State(
models: Map[String, Document_Model] = Map.empty,
- pending_input: Set[Document.Node.Name] = Set.empty,
- pending_output: Set[Document.Node.Name] = Set.empty)
+ pending_input: Set[String] = Set.empty,
+ pending_output: Set[String] = Set.empty)
}
class VSCode_Resources(
val options: Options,
+ val text_length: Text.Length,
loaded_theories: Set[String],
known_theories: Map[String, Document.Node.Name],
base_syntax: Outer_Syntax)
@@ -59,14 +60,39 @@
def get_model(uri: String): Option[Document_Model] = state.value.models.get(uri)
- def update_model(model: Document_Model)
+ def update_model(session: Session, uri: String, text: String)
{
state.change(st =>
- st.copy(
- models = st.models + (model.node_name.node -> model),
- pending_input = st.pending_input + model.node_name))
+ {
+ val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
+ val model1 = (model.update_text(text) getOrElse model).copy(external = false)
+ st.copy(
+ models = st.models + (uri -> model1),
+ pending_input = st.pending_input + uri)
+ })
}
+ def close_model(uri: String): Option[Document_Model] =
+ state.change_result(st =>
+ st.models.get(uri) match {
+ case None => (None, st)
+ case Some(model) =>
+ (Some(model), st.copy(models = st.models + (uri -> model.copy(external = true))))
+ })
+
+ def sync_external(changed_files: Set[JFile]): Boolean =
+ state.change_result(st =>
+ {
+ val changed =
+ (for {
+ (uri, model) <- st.models.iterator
+ if changed_files(model.file)
+ model1 <- model.update_file
+ } yield (uri, model)).toList
+ if (changed.isEmpty) (false, st)
+ else (true, st.copy(models = (st.models /: changed)(_ + _)))
+ })
+
/* pending input */
@@ -76,13 +102,14 @@
{
val changed =
(for {
- node_name <- st.pending_input.iterator
- model <- st.models.get(node_name.node)
- if model.changed } yield model).toList
- val edits = for { model <- changed; edit <- model.node_edits } yield edit
- session.update(Document.Blobs.empty, edits)
+ uri <- st.pending_input.iterator
+ model <- st.models.get(uri)
+ res <- model.flush_edits
+ } yield res).toList
+
+ session.update(Document.Blobs.empty, changed.flatMap(_._1))
st.copy(
- models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
+ models = (st.models /: changed) { case (ms, (_, m)) => ms + (m.uri -> m) },
pending_input = Set.empty)
})
}
@@ -90,7 +117,7 @@
/* pending output */
- def update_output(changed_nodes: Set[Document.Node.Name]): Unit =
+ def update_output(changed_nodes: List[String]): Unit =
state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
def flush_output(channel: Channel)
@@ -99,8 +126,8 @@
{
val changed_iterator =
for {
- node_name <- st.pending_output.iterator
- model <- st.models.get(node_name.node)
+ uri <- st.pending_output.iterator
+ model <- st.models.get(uri)
rendering = model.rendering()
(diagnostics, model1) <- model.publish_diagnostics(rendering)
} yield {