src/Tools/jEdit/src/jedit_editor.scala
changeset 55432 9c53198dbb1c
parent 54706 d3c656f0b7ab
child 55781 b3a4207fb9a6
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Feb 11 17:44:29 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Feb 11 21:58:31 2014 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4      val buffer = view.getBuffer
     1.5  
     1.6      PIDE.document_view(text_area) match {
     1.7 -      case Some(doc_view) =>
     1.8 +      case Some(doc_view) if doc_view.model.is_theory =>
     1.9          val node = snapshot.version.nodes(doc_view.model.node_name)
    1.10          val caret = snapshot.revert(text_area.getCaretPosition)
    1.11          if (caret < buffer.getLength) {
    1.12 @@ -81,7 +81,7 @@
    1.13            else None
    1.14          }
    1.15          else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    1.16 -      case None =>
    1.17 +      case _ =>
    1.18          PIDE.document_model(buffer) match {
    1.19            case Some(model) if !model.is_theory =>
    1.20              snapshot.version.nodes.thy_load_commands(model.node_name) match {