# HG changeset patch
# User wenzelm
# Date 1230492654 -3600
# Node ID 57fce8528a22aaa167df72c0bb657afce7ef4d00
# Parent  39cb4ed5183bb64b27de4ceb9569f926c39029bc
added central id generator;

diff -r 39cb4ed5183b -r 57fce8528a22 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Dec 28 19:37:51 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Dec 28 20:30:54 2008 +0100
@@ -69,6 +69,12 @@
   }
 
 
+  /* unique ids */  // FIXME specific to "session" (!??)
+
+  private var id_count: BigInt = 0
+  def id() : String = synchronized { id_count += 1; "editor:" + id_count }
+
+
   // mapping buffer <-> prover
 
   private val mapping = new HashMap[JEditBuffer, ProverSetup]