tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
--- 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) <-