# HG changeset patch
# User wenzelm
# Date 1483652286 -3600
# Node ID a0e1f64be67cb1f1b5e3bc0787d8975bfc9eeda7
# Parent  8e7db8df16a041d7496610dfc38be577b06f16aa# Parent  81a5473e6d047295caf670984c36c6facafb85b0
merged

diff -r 8e7db8df16a0 -r a0e1f64be67c src/Pure/General/file_watcher.scala
--- 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
+    }
   }
 }
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Pure/PIDE/command.scala
--- 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
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Pure/PIDE/document.scala
--- 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))
             }
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Pure/PIDE/line.scala
--- 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))
+    }
   }
 
 
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Pure/PIDE/resources.scala
--- 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(
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Pure/PIDE/session.scala
--- 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()
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Pure/Thy/thy_syntax.scala
--- 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
             })
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/VSCode/extension/isabelle-ml-grammar.json
--- 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": {
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/VSCode/extension/package.json
--- 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" },
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/VSCode/src/document_model.scala
--- 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
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/VSCode/src/grammar.scala
--- 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) + """
     },
     {
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/VSCode/src/server.scala
--- 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)
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/VSCode/src/vscode_rendering.scala
--- 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")
 
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/VSCode/src/vscode_resources.scala
--- 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)
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/jEdit/src/document_model.scala
--- 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,
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/jEdit/src/document_view.scala
--- 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()
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/jEdit/src/jedit_editor.scala
--- 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
             }
diff -r 8e7db8df16a0 -r a0e1f64be67c src/Tools/jEdit/src/jedit_resources.scala
--- 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)