# HG changeset patch
# User wenzelm
# Date 1412327788 -7200
# Node ID f008ceb3b0464f409b3fdd315655a8b0ba9c8468
# Parent  f805b366a4979bc5d18fc113ab6745244750009d
more buffer.isEditable checks;

diff -r f805b366a497 -r f008ceb3b046 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Oct 03 11:03:37 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala	Fri Oct 03 11:16:28 2014 +0200
@@ -60,16 +60,18 @@
                 }
 
               case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
-                props match {
-                  case Position.Id(id) =>
-                    Isabelle.edit_command(snapshot, buffer,
-                      props.exists(_ == Markup.PADDING_COMMAND), id, text)
-                  case _ =>
-                    if (props.exists(_ == Markup.PADDING_LINE))
-                      Isabelle.insert_line_padding(text_area, text)
-                    else text_area.setSelectedText(text)
+                if (buffer.isEditable) {
+                  props match {
+                    case Position.Id(id) =>
+                      Isabelle.edit_command(snapshot, buffer,
+                        props.exists(_ == Markup.PADDING_COMMAND), id, text)
+                    case _ =>
+                      if (props.exists(_ == Markup.PADDING_LINE))
+                        Isabelle.insert_line_padding(text_area, text)
+                      else text_area.setSelectedText(text)
+                  }
+                  text_area.requestFocus
                 }
-                text_area.requestFocus
 
               case Protocol.Dialog(id, serial, result) =>
                 model.session.dialog_result(id, serial, result)
diff -r f805b366a497 -r f008ceb3b046 src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala	Fri Oct 03 11:03:37 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala	Fri Oct 03 11:16:28 2014 +0200
@@ -75,7 +75,7 @@
       case text_area: TextArea =>
         text_area.getBuffer match {
           case buffer: Buffer
-          if (JEdit_Lib.buffer_name(buffer).endsWith(".bib")) =>
+          if (JEdit_Lib.buffer_name(buffer).endsWith(".bib") && buffer.isEditable) =>
             val menu = new JMenu("BibTeX entries")
             for (entry <- Bibtex.entries) {
               val item = new JMenuItem(entry.name)