src/Tools/jEdit/src/document_model.scala
changeset 64799 c0c648911f1a
parent 64680 7f87c1aa0ffa
child 64813 7283f41d05ab
--- 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,