# HG changeset patch
# User wenzelm
# Date 1395063443 -3600
# Node ID 0bc9b0ad62876b1f3196864063178af4d9843dd0
# Parent  79c29244b377935a04e61aab5e5df0a6f65a6ba2
tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;

diff -r 79c29244b377 -r 0bc9b0ad6287 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Mar 17 13:53:02 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Mar 17 14:37:23 2014 +0100
@@ -422,6 +422,7 @@
     val node_name: Node.Name
     val node: Node
     val thy_load_commands: List[Command]
+    def is_loaded: Boolean
     def eq_content(other: Snapshot): Boolean
 
     def cumulate[A](
@@ -681,6 +682,8 @@
           if (node_name.is_theory) Nil
           else version.nodes.thy_load_commands(node_name)
 
+        val is_loaded: Boolean = node_name.is_theory || !thy_load_commands.isEmpty
+
         def eq_content(other: Snapshot): Boolean =
         {
           def eq_commands(commands: (Command, Command)): Boolean =
diff -r 79c29244b377 -r 0bc9b0ad6287 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 17 13:53:02 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 17 14:37:23 2014 +0100
@@ -599,7 +599,7 @@
 
   def background(range: Text.Range): List[Text.Info[Color]] =
   {
-    if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
+    if (snapshot.is_outdated && snapshot.is_loaded) List(Text.Info(range, outdated_color))
     else
       for {
         Text.Info(r, result) <-