--- a/src/Tools/jEdit/src/document_model.scala Wed Nov 20 15:53:59 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Wed Nov 20 16:15:54 2013 +0100
@@ -88,7 +88,7 @@
def node_required_=(b: Boolean)
{
Swing_Thread.require()
- if (_node_required != b) {
+ if (_node_required != b && is_theory) {
_node_required = b
PIDE.options_changed()
PIDE.editor.flush()
--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Nov 20 15:53:59 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Nov 20 16:15:54 2013 +0100
@@ -80,7 +80,7 @@
else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
case None =>
PIDE.document_model(buffer) match {
- case Some(model) if !model.node_name.is_theory =>
+ case Some(model) if !model.is_theory =>
snapshot.version.nodes.thy_load_commands(model.node_name) match {
case cmd :: _ => Some(cmd)
case Nil => None
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Nov 20 15:53:59 2013 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Nov 20 16:15:54 2013 +0100
@@ -186,10 +186,10 @@
val snapshot = PIDE.session.snapshot()
val iterator =
- restriction match {
+ (restriction match {
case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
case None => snapshot.version.nodes.entries
- }
+ }).filter(_._1.is_theory)
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
if (PIDE.thy_load.loaded_theories(name.theory)) status