src/Tools/jEdit/src/jedit_thy_load.scala

--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 16:24:52 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 18:04:30 2012 +0200
@@ -33,6 +33,23 @@
     }
   }
 
+  override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+  {
+    Swing_Thread.now {
+      Isabelle.jedit_buffer(name.node) match {
+        case Some(buffer) =>
+          Isabelle.buffer_lock(buffer) {
+            Some(f(buffer.getSegment(0, buffer.getLength)))
+          }
+        case None => None
+      }
+    } getOrElse {
+      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
+      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+      f(File.read(file))
+    }
+  }
+
   def check_file(view: View, path: String): Boolean =
   {
     val vfs = VFSManager.getVFSForPath(path)
@@ -52,23 +69,5 @@
       catch { case _: IOException => }
     }
   }
-
-  override def check_thy(syntax: Outer_Syntax, name: Document.Node.Name)
-    : Document.Node.Header =
-  {
-    Swing_Thread.now {
-      Isabelle.jedit_buffer(name.node) match {
-        case Some(buffer) =>
-          Isabelle.buffer_lock(buffer) {
-            Some(check_thy_text(syntax, name, buffer.getSegment(0, buffer.getLength)))
-          }
-        case None => None
-      }
-    } getOrElse {
-      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
-      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
-      check_thy_text(syntax, name, File.read(file))
-    }
-  }
 }