tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
authorwenzelm
Mon, 17 Mar 2014 14:37:23 +0100
changeset 56176 0bc9b0ad6287
parent 56175 79c29244b377
child 56177 bfa9dfb722de
tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/rendering.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 =
--- 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) <-