--- a/src/Tools/jEdit/src/jedit_thy_load.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Mon Sep 17 17:49:11 2012 +0200
@@ -36,9 +36,9 @@
override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
{
Swing_Thread.now {
- Isabelle.jedit_buffer(name.node) match {
+ JEdit_Lib.jedit_buffer(name.node) match {
case Some(buffer) =>
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
Some(f(buffer.getSegment(0, buffer.getLength)))
}
case None => None