1.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Nov 20 15:53:59 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Nov 20 16:15:54 2013 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4    def node_required_=(b: Boolean)
     1.5    {
     1.6      Swing_Thread.require()
     1.7 -    if (_node_required != b) {
     1.8 +    if (_node_required != b && is_theory) {
     1.9        _node_required = b
    1.10        PIDE.options_changed()
    1.11        PIDE.editor.flush()

     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 20 15:53:59 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 20 16:15:54 2013 +0100
     2.3 @@ -80,7 +80,7 @@
     2.4          else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
     2.5        case None =>
     2.6          PIDE.document_model(buffer) match {
     2.7 -          case Some(model) if !model.node_name.is_theory =>
     2.8 +          case Some(model) if !model.is_theory =>
     2.9              snapshot.version.nodes.thy_load_commands(model.node_name) match {
    2.10                case cmd :: _ => Some(cmd)
    2.11                case Nil => None

     3.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Nov 20 15:53:59 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Nov 20 16:15:54 2013 +0100
     3.3 @@ -186,10 +186,10 @@
     3.4      val snapshot = PIDE.session.snapshot()
     3.5  
     3.6      val iterator =
     3.7 -      restriction match {
     3.8 +      (restriction match {
     3.9          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
    3.10          case None => snapshot.version.nodes.entries
    3.11 -      }
    3.12 +      }).filter(_._1.is_theory)
    3.13      val nodes_status1 =
    3.14        (nodes_status /: iterator)({ case (status, (name, node)) =>
    3.15            if (PIDE.thy_load.loaded_theories(name.theory)) status