tuned property name;
authorwenzelm
Sun Dec 16 18:02:28 2012 +0100 (2012-12-16)
changeset 50565b00ea974613c
parent 50564 c6fde2fc4217
child 50566 b43c4f660320
tuned property name;
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Dec 16 17:38:16 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Dec 16 18:02:28 2012 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  {
     1.5    /* document model of buffer */
     1.6  
     1.7 -  private val key = "isabelle.document_model"
     1.8 +  private val key = "PIDE.document_model"
     1.9  
    1.10    def apply(buffer: Buffer): Option[Document_Model] =
    1.11    {