# HG changeset patch
# User wenzelm
# Date 1355677348 -3600
# Node ID b00ea974613c8446e8be6a660e759bd5fbed739c
# Parent  c6fde2fc421756fba44c87d54af693280bdb4c8d
tuned property name;

diff -r c6fde2fc4217 -r b00ea974613c src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Dec 16 17:38:16 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Dec 16 18:02:28 2012 +0100
@@ -23,7 +23,7 @@
 {
   /* document model of buffer */
 
-  private val key = "isabelle.document_model"
+  private val key = "PIDE.document_model"
 
   def apply(buffer: Buffer): Option[Document_Model] =
   {