# HG changeset patch
# User wenzelm
# Date 1384959239 -3600
# Node ID 2c1440f70028d3efaec7ff43d71341750a96f95d
# Parent  2ea4d717d15214d5e7b0cb2e1d736ff5c7879ff7
ranges of thy_load commands count as visible within perspective;
convert ranges wrt. snapshot -- relevant for outdated situation;

diff -r 2ea4d717d152 -r 2c1440f70028 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Nov 20 15:00:25 2013 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Nov 20 15:53:59 2013 +0100
@@ -239,6 +239,9 @@
 
   /* blobs */
 
+  def blobs_names: List[Document.Node.Name] =
+    for (Exn.Res((name, _)) <- blobs) yield name
+
   def blobs_digests: List[SHA1.Digest] =
     for (Exn.Res((_, Some(digest))) <- blobs) yield digest
 
diff -r 2ea4d717d152 -r 2c1440f70028 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Nov 20 15:00:25 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Nov 20 15:53:59 2013 +0100
@@ -257,7 +257,7 @@
       (for {
         (_, node) <- entries
         cmd <- node.thy_load_commands.iterator
-        Exn.Res((name, _)) <- cmd.blobs.iterator
+        name <- cmd.blobs_names.iterator
         if name == file_name
       } yield cmd).toList
 
diff -r 2ea4d717d152 -r 2c1440f70028 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Nov 20 15:00:25 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Nov 20 15:53:59 2013 +0100
@@ -104,11 +104,26 @@
 
     if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()
-      Document.Node.Perspective(node_required, Text.Perspective(
+
+      val document_view_ranges =
         for {
           doc_view <- PIDE.document_views(buffer)
           range <- doc_view.perspective(snapshot).ranges
-        } yield range), PIDE.editor.node_overlays(node_name))
+        } yield range
+
+      val thy_load_ranges =
+        for {
+          cmd <- snapshot.node.thy_load_commands
+          blob_name <- cmd.blobs_names
+          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
+          if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
+          start <- snapshot.node.command_start(cmd)
+          range = snapshot.convert(cmd.proper_range + start)
+        } yield range
+
+      Document.Node.Perspective(node_required,
+        Text.Perspective(document_view_ranges ::: thy_load_ranges),
+        PIDE.editor.node_overlays(node_name))
     }
     else empty_perspective
   }
diff -r 2ea4d717d152 -r 2c1440f70028 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Nov 20 15:00:25 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Nov 20 15:53:59 2013 +0100
@@ -82,7 +82,7 @@
         PIDE.editor.current_command(view, snapshot) match {
           case Some(command) =>
             snapshot.node.command_start(command) match {
-              case Some(start) => List(command.proper_range + start)
+              case Some(start) => List(snapshot.convert(command.proper_range + start))
               case None => Nil
             }
           case None => Nil