# HG changeset patch
# User wenzelm
# Date 1314126899 -7200
# Node ID 3b9b684bfa6fe5e2dfc9be664419216a5f91499d
# Parent  9fbee4aab115f806e20b631eec09e88d02a8f229
handle potentially more approriate BufferUpdate.LOADED event;

diff -r 9fbee4aab115 -r 3b9b684bfa6f src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 23:39:05 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 23 21:14:59 2011 +0200
@@ -409,7 +409,7 @@
           Isabelle.start_session()
 
       case msg: BufferUpdate
-      if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+      if msg.getWhat == BufferUpdate.LOADED =>
 
         val buffer = msg.getBuffer
         if (buffer != null && Isabelle.session.is_ready)