# HG changeset patch
# User wenzelm
# Date 1483615405 -3600
# Node ID c0c648911f1aa2d83c6418b00b8fbe55964b573e
# Parent  0e5ec80c352a116ba13d6b952eba7ebdf6b13128
misc tuning and clarification;

diff -r 0e5ec80c352a -r c0c648911f1a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Jan 05 10:49:47 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 05 12:23:25 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
@@ -443,8 +445,8 @@
 
     def node_name: Node.Name
     def node: Node
-    def load_commands: List[Command]
-    def is_loaded: Boolean
+    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)
@@ -771,13 +773,19 @@
         def revert(range: Text.Range) = range.map(revert(_))
 
         val node_name: Node.Name = name
-        def node: Node = version.nodes(name)
+        val node: Node = version.nodes(name)
 
-        val load_commands: List[Command] =
+        val commands_loading: List[Command] =
           if (node_name.is_theory) Nil
-          else version.nodes.load_commands(node_name)
+          else version.nodes.commands_loading(node_name)
 
-        def 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 */
@@ -816,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 0e5ec80c352a -r c0c648911f1a src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Jan 05 10:49:47 2017 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Jan 05 12:23:25 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 0e5ec80c352a -r c0c648911f1a src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Jan 05 10:49:47 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jan 05 12:23:25 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 0e5ec80c352a -r c0c648911f1a src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Jan 05 10:49:47 2017 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Jan 05 12:23:25 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 0e5ec80c352a -r c0c648911f1a src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Jan 05 10:49:47 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Jan 05 12:23:25 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
             }