# HG changeset patch
# User wenzelm
# Date 1384960554 -3600
# Node ID 8330faaeebd59bbefaec66f1923834095aa47be9
# Parent  2c1440f70028d3efaec7ff43d71341750a96f95d
restrict node_required status and Theories panel to actual theories;

diff -r 2c1440f70028 -r 8330faaeebd5 src/Tools/jEdit/src/document_model.scala
--- 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()
diff -r 2c1440f70028 -r 8330faaeebd5 src/Tools/jEdit/src/jedit_editor.scala
--- 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
diff -r 2c1440f70028 -r 8330faaeebd5 src/Tools/jEdit/src/theories_dockable.scala
--- 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