--- a/src/Pure/General/file_watcher.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Pure/General/file_watcher.scala Thu Jan 05 22:38:06 2017 +0100
@@ -15,100 +15,109 @@
import scala.collection.JavaConversions
+class File_Watcher private[File_Watcher] // dummy template
+{
+ def register(dir: JFile) { }
+ def register_parent(file: JFile) { }
+ def deregister(dir: JFile) { }
+ def shutdown() { }
+}
+
object File_Watcher
{
def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
- new File_Watcher(handle, delay)
+ if (Platform.is_windows) new File_Watcher
+ else new Impl(handle, delay)
- /* internal state */
+ /* proper implementation */
sealed case class State(
dirs: Map[JFile, WatchKey] = Map.empty,
changed: Set[JFile] = Set.empty)
-}
-class File_Watcher private(handle: Set[JFile] => Unit, delay: Time)
-{
- private val state = Synchronized(File_Watcher.State())
- private val watcher = FileSystems.getDefault.newWatchService()
+ class Impl private[File_Watcher](handle: Set[JFile] => Unit, delay: Time) extends File_Watcher
+ {
+ private val state = Synchronized(File_Watcher.State())
+ private val watcher = FileSystems.getDefault.newWatchService()
- /* registered directories */
+ /* registered directories */
- def register(dir: JFile): Unit =
- state.change(st =>
- st.dirs.get(dir) match {
- case Some(key) if key.isValid => st
- case _ =>
- val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY)
- st.copy(dirs = st.dirs + (dir -> key))
- })
+ override def register(dir: JFile): Unit =
+ state.change(st =>
+ st.dirs.get(dir) match {
+ case Some(key) if key.isValid => st
+ case _ =>
+ val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY)
+ st.copy(dirs = st.dirs + (dir -> key))
+ })
- def register_parent(file: JFile): Unit =
- {
- val dir = file.getParentFile
- if (dir != null && dir.isDirectory) register(dir)
- }
+ override def register_parent(file: JFile): Unit =
+ {
+ val dir = file.getParentFile
+ if (dir != null && dir.isDirectory) register(dir)
+ }
- def deregister(dir: JFile): Unit =
- state.change(st =>
- st.dirs.get(dir) match {
- case None => st
- case Some(key) =>
- key.cancel
- st.copy(dirs = st.dirs - dir)
- })
+ override def deregister(dir: JFile): Unit =
+ state.change(st =>
+ st.dirs.get(dir) match {
+ case None => st
+ case Some(key) =>
+ key.cancel
+ st.copy(dirs = st.dirs - dir)
+ })
- /* changed directory entries */
+ /* changed directory entries */
- private val delay_changed = Standard_Thread.delay_last(delay)
- {
- val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
- handle(changed)
- }
+ private val delay_changed = Standard_Thread.delay_last(delay)
+ {
+ val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
+ handle(changed)
+ }
- private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
- {
- try {
- while (true) {
- val key = watcher.take
- val has_changed =
- state.change_result(st =>
- {
- val (remove, changed) =
- st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
- case Some(dir) =>
- val events =
- JavaConversions.collectionAsScalaIterable(
- key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
- val remove = if (key.reset) None else Some(dir)
- val changed =
- (Set.empty[JFile] /: events.iterator) {
- case (set, event) => set + dir.toPath.resolve(event.context).toFile
- }
- (remove, changed)
- case None =>
- key.pollEvents
- key.reset
- (None, Set.empty[JFile])
- }
- (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
- })
- if (has_changed) delay_changed.invoke()
+ private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
+ {
+ try {
+ while (true) {
+ val key = watcher.take
+ val has_changed =
+ state.change_result(st =>
+ {
+ val (remove, changed) =
+ st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
+ case Some(dir) =>
+ val events =
+ JavaConversions.collectionAsScalaIterable(
+ key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
+ val remove = if (key.reset) None else Some(dir)
+ val changed =
+ (Set.empty[JFile] /: events.iterator) {
+ case (set, event) => set + dir.toPath.resolve(event.context).toFile
+ }
+ (remove, changed)
+ case None =>
+ key.pollEvents
+ key.reset
+ (None, Set.empty[JFile])
+ }
+ (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
+ })
+ if (has_changed) delay_changed.invoke()
+ }
}
+ catch { case Exn.Interrupt() => }
}
- catch { case Exn.Interrupt() => }
- }
- /* shutdown */
+ /* shutdown */
- def shutdown()
- {
- watcher_thread.interrupt
- watcher_thread.join
- delay_changed.revoke
+ override def shutdown()
+ {
+ watcher_thread.interrupt
+ watcher_thread.join
+ delay_changed.revoke
+ }
}
}
--- a/src/Pure/PIDE/command.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Pure/PIDE/command.scala Thu Jan 05 22:38:06 2017 +0100
@@ -36,6 +36,7 @@
final class Results private(private val rep: SortedMap[Long, XML.Tree])
{
+ def is_empty: Boolean = rep.isEmpty
def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
def get(serial: Long): Option[XML.Tree] = rep.get(serial)
def iterator: Iterator[Results.Entry] = rep.iterator
--- a/src/Pure/PIDE/document.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Pure/PIDE/document.scala Thu Jan 05 22:38:06 2017 +0100
@@ -24,7 +24,7 @@
final class Overlays private(rep: Map[Node.Name, Node.Overlays])
{
- def apply(name: Document.Node.Name): Node.Overlays =
+ def apply(name: Node.Name): Node.Overlays =
rep.getOrElse(name, Node.Overlays.empty)
private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays =
@@ -261,10 +261,12 @@
def commands: Linear_Set[Command] = _commands.commands
def load_commands: List[Command] = _commands.load_commands
+ def load_commands_changed(doc_blobs: Blobs): Boolean =
+ load_commands.exists(_.blobs_changed(doc_blobs))
def clear: Node = new Node(header = header, syntax = syntax)
- def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
+ def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged))
def update_header(new_header: Node.Header): Node =
new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
@@ -340,7 +342,7 @@
def iterator: Iterator[(Node.Name, Node)] =
graph.iterator.map({ case (name, (node, _)) => (name, node) })
- def load_commands(file_name: Node.Name): List[Command] =
+ def commands_loading(file_name: Node.Name): List[Command] =
(for {
(_, node) <- iterator
cmd <- node.load_commands.iterator
@@ -348,14 +350,6 @@
if name == file_name
} yield cmd).toList
- def undefined_blobs(pred: Node.Name => Boolean): List[Node.Name] =
- (for {
- (node_name, node) <- iterator
- if pred(node_name)
- cmd <- node.load_commands.iterator
- name <- cmd.blobs_undefined.iterator
- } yield name).toList
-
def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
def topological_order: List[Node.Name] = graph.topological_order
@@ -440,19 +434,19 @@
abstract class Snapshot
{
- val state: State
- val version: Version
- val is_outdated: Boolean
+ def state: State
+ def version: Version
+ def is_outdated: Boolean
def convert(i: Text.Offset): Text.Offset
def revert(i: Text.Offset): Text.Offset
def convert(range: Text.Range): Text.Range
def revert(range: Text.Range): Text.Range
- val node_name: Node.Name
- val node: Node
- val load_commands: List[Command]
- def is_loaded: Boolean
+ def node_name: Node.Name
+ def node: Node
+ def commands_loading: List[Command]
+ def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
def find_command(id: Document_ID.Generic): Option[(Node, Command)]
def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
@@ -763,9 +757,9 @@
{
/* global information */
- val state = State.this
- val version = stable.version.get_finished
- val is_outdated = pending_edits.nonEmpty || latest != stable
+ val state: State = State.this
+ val version: Version = stable.version.get_finished
+ val is_outdated: Boolean = pending_edits.nonEmpty || latest != stable
/* local node content */
@@ -778,14 +772,20 @@
def convert(range: Text.Range) = range.map(convert(_))
def revert(range: Text.Range) = range.map(revert(_))
- val node_name = name
- val node = version.nodes(name)
+ val node_name: Node.Name = name
+ val node: Node = version.nodes(name)
+
+ val commands_loading: List[Command] =
+ if (node_name.is_theory) Nil
+ else version.nodes.commands_loading(node_name)
- val load_commands: List[Command] =
- if (node_name.is_theory) Nil
- else version.nodes.load_commands(node_name)
-
- val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
+ def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] =
+ (for {
+ cmd <- node.load_commands.iterator
+ blob_name <- cmd.blobs_names.iterator
+ if pred(blob_name)
+ start <- node.command_start(cmd)
+ } yield convert(cmd.proper_range + start)).toList
/* find command */
@@ -824,7 +824,7 @@
{
val former_range = revert(range).inflate_singularity
val (chunk_name, command_iterator) =
- load_commands match {
+ commands_loading match {
case command :: _ => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
case _ => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
}
--- a/src/Pure/PIDE/line.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Pure/PIDE/line.scala Thu Jan 05 22:38:06 2017 +0100
@@ -12,6 +12,15 @@
object Line
{
+ /* logical lines */
+
+ def normalize(text: String): String =
+ if (text.contains('\r')) text.replace("\r\n", "\n") else text
+
+ def logical_lines(text: String): List[String] =
+ Library.split_lines(normalize(text))
+
+
/* position */
object Position
@@ -34,7 +43,7 @@
def advance(text: String, text_length: Text.Length): Position =
if (text.isEmpty) this
else {
- val lines = Library.split_lines(text)
+ val lines = logical_lines(text)
val l = line + lines.length - 1
val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last))
Position(l, c)
@@ -81,10 +90,7 @@
object Document
{
def apply(text: String, text_length: Text.Length): Document =
- if (text.contains('\r'))
- Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))), text_length)
- else
- Document(Library.split_lines(text).map(s => Line(s)), text_length)
+ Document(logical_lines(text).map(Line(_)), text_length)
}
sealed case class Document(lines: List[Line], text_length: Text.Length)
@@ -136,6 +142,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))
+ }
}
--- a/src/Pure/PIDE/resources.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Thu Jan 05 22:38:06 2017 +0100
@@ -162,6 +162,17 @@
else None
+ /* blobs */
+
+ def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
+ (for {
+ (node_name, node) <- nodes.iterator
+ if !loaded_theories(node_name.theory)
+ cmd <- node.load_commands.iterator
+ name <- cmd.blobs_undefined.iterator
+ } yield name).toList
+
+
/* document changes */
def parse_change(
--- a/src/Pure/PIDE/session.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Pure/PIDE/session.scala Thu Jan 05 22:38:06 2017 +0100
@@ -297,6 +297,7 @@
assignment |= assign
for (command <- cmds) {
nodes += command.node_name
+ command.blobs_names.foreach(nodes += _)
commands += command
}
delay_flush.invoke()
--- a/src/Pure/Thy/thy_syntax.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Thu Jan 05 22:38:06 2017 +0100
@@ -307,7 +307,7 @@
val reparse =
(syntax_changed /: nodes0.iterator)({
case (reparse, (name, node)) =>
- if (node.load_commands.exists(_.blobs_changed(doc_blobs)) && !reparse.contains(name))
+ if (node.load_commands_changed(doc_blobs) && !reparse.contains(name))
name :: reparse
else reparse
})
--- a/src/Tools/VSCode/extension/isabelle-ml-grammar.json Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/VSCode/extension/isabelle-ml-grammar.json Thu Jan 05 22:38:06 2017 +0100
@@ -1,7 +1,7 @@
{
"name": "Isabelle/ML",
"scopeName": "source.isabelle-ml",
- "fileTypes": ["ML"],
+ "fileTypes": ["ML", "sml", "sig"],
"uuid": "aa32eb5e-d0d9-11e6-b7a4-37ba001f1e6e",
"keyEquivalent": "^~M",
"repository": {
@@ -190,7 +190,7 @@
"begin": "\\b(fun|and)\\s+([\\w]+)\\b",
"patterns": [
{
- "include": "source.ml"
+ "include": "source.isabelle-ml"
}
],
"captures": {
--- a/src/Tools/VSCode/extension/package.json Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json Thu Jan 05 22:38:06 2017 +0100
@@ -10,7 +10,7 @@
"document preparation"
],
"icon": "isabelle.png",
- "version": "0.3.0",
+ "version": "0.4.0",
"publisher": "makarius",
"license": "BSD-3-Clause",
"repository": { "url": "http://isabelle.in.tum.de/repos/isabelle" },
--- a/src/Tools/VSCode/src/document_model.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Thu Jan 05 22:38:06 2017 +0100
@@ -45,6 +45,8 @@
def external(b: Boolean): Document_Model = copy(external_file = b)
+ def node_visible: Boolean = !external_file
+
/* header */
@@ -60,19 +62,39 @@
/* 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 */
- def update_text(new_text: String): Option[Document_Model] =
+ def update_text(text: String): Option[Document_Model] =
{
+ val new_text = Line.normalize(text)
val old_text = doc.make_text
if (new_text == old_text) None
else {
@@ -84,17 +106,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
--- a/src/Tools/VSCode/src/grammar.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala Thu Jan 05 22:38:06 2017 +0100
@@ -93,7 +93,7 @@
"match": """ + grouped_names(operators) + """
},
{
- "name": "constant.language.isabelle",
+ "name": "entity.name.function.isabelle",
"match": """ + grouped_names(keywords3) + """
},
{
--- a/src/Tools/VSCode/src/server.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala Thu Jan 05 22:38:06 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) {
@@ -331,12 +335,12 @@
case Protocol.Initialize(id) => init(id)
case Protocol.Shutdown(id) => shutdown(id)
case Protocol.Exit(()) => exit()
- case Protocol.DidOpenTextDocument(uri, lang, version, text) =>
- update_document(uri, text)
- case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
- update_document(uri, text)
- case Protocol.DidCloseTextDocument(uri) =>
- close_document(uri)
+ 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.Hover(id, node_pos) => hover(id, node_pos)
case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
--- a/src/Tools/VSCode/src/vscode_rendering.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Thu Jan 05 22:38:06 2017 +0100
@@ -53,7 +53,7 @@
if body.nonEmpty => Some(res + (i -> msg))
case _ => None
- })
+ }).filterNot(info => info.info.is_empty)
val diagnostics_margin = options.int("vscode_diagnostics_margin")
--- a/src/Tools/VSCode/src/vscode_resources.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Jan 05 22:38:06 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 =>
@@ -120,7 +134,7 @@
/* file content */
def try_read(file: JFile): Option[String] =
- try { Some(File.read(file)) }
+ try { Some(Line.normalize(File.read(file))) }
catch { case ERROR(_) => None }
def get_file_content(file: JFile): Option[String] =
@@ -134,34 +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)
- _ = watcher.register_parent(file)
- text <- try_read(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)))
})
}
@@ -176,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)
--- a/src/Tools/jEdit/src/document_model.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Thu Jan 05 22:38:06 2017 +0100
@@ -119,7 +119,8 @@
}
}
- def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
+ def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs)
+ : (Boolean, Document.Node.Perspective_Text) =
{
GUI_Thread.require {}
@@ -132,17 +133,8 @@
range <- doc_view.perspective(snapshot).ranges
} yield range
- val load_ranges =
- for {
- cmd <- snapshot.node.load_commands
- blob_name <- cmd.blobs_names
- blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
- if JEdit_Lib.jedit_text_areas(blob_buffer).nonEmpty
- start <- snapshot.node.command_start(cmd)
- range = snapshot.convert(cmd.proper_range + start)
- } yield range
-
- val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs))
+ val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
+ val reparse = snapshot.node.load_commands_changed(doc_blobs)
(reparse,
Document.Node.Perspective(node_required,
--- a/src/Tools/jEdit/src/document_view.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Thu Jan 05 22:38:06 2017 +0100
@@ -212,10 +212,8 @@
if (model.buffer == text_area.getBuffer) {
val snapshot = model.snapshot()
- val load_changed =
- snapshot.load_commands.exists(changed.commands.contains)
-
- if (changed.assignment || load_changed ||
+ if (changed.assignment ||
+ snapshot.commands_loading.exists(changed.commands.contains) ||
(changed.nodes.contains(model.node_name) &&
changed.commands.exists(snapshot.node.commands.contains)))
text_overview.invoke()
--- a/src/Tools/jEdit/src/jedit_editor.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Jan 05 22:38:06 2017 +0100
@@ -60,6 +60,12 @@
else None
}
+ def visible_node(name: Document.Node.Name): Boolean =
+ JEdit_Lib.jedit_buffer(name) match {
+ case Some(buffer) => JEdit_Lib.jedit_text_areas(buffer).nonEmpty
+ case None => false
+ }
+
/* current situation */
@@ -109,7 +115,7 @@
case _ =>
PIDE.document_model(buffer) match {
case Some(model) if !model.is_theory =>
- snapshot.version.nodes.load_commands(model.node_name) match {
+ snapshot.version.nodes.commands_loading(model.node_name) match {
case cmd :: _ => Some(cmd)
case Nil => None
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Thu Jan 05 17:11:21 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Jan 05 22:38:06 2017 +0100
@@ -111,9 +111,6 @@
/* theory text edits */
- def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
- nodes.undefined_blobs(node => !loaded_theories(node.theory))
-
override def commit(change: Session.Change)
{
if (change.syntax_changed.nonEmpty)