# HG changeset patch
# User wenzelm
# Date 1314697427 -7200
# Node ID 96b6388d06c47b0047b29aae3acdd7dfd6ad5307
# Parent  f23ac1a679d1ec91076ea3f170bd80e0bdec3bc5
separate module for jEdit primitives for loading theory files;

diff -r f23ac1a679d1 -r 96b6388d06c4 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Mon Aug 29 22:10:08 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Aug 30 11:43:47 2011 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Thy/thy_load.scala
     Author:     Makarius
 
-Loading files that contribute to a theory.
+Primitives for loading theory files.
 */
 
 package isabelle
diff -r f23ac1a679d1 -r 96b6388d06c4 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 29 22:10:08 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 30 11:43:47 2011 +0200
@@ -17,6 +17,7 @@
   "src/isabelle_markup.scala"
   "src/isabelle_options.scala"
   "src/isabelle_sidekick.scala"
+  "src/jedit_thy_load.scala"
   "src/output_dockable.scala"
   "src/plugin.scala"
   "src/protocol_dockable.scala"
diff -r f23ac1a679d1 -r 96b6388d06c4 src/Tools/jEdit/src/jedit_thy_load.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 30 11:43:47 2011 +0200
@@ -0,0 +1,68 @@
+/*  Title:      Tools/jEdit/src/plugin.scala
+    Author:     Makarius
+
+Primitives for loading theory files, based on jEdit buffer content.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.io.File
+import javax.swing.text.Segment
+
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
+import org.gjt.sp.jedit.MiscUtilities
+
+
+class JEdit_Thy_Load extends Thy_Load
+{
+  /* loaded theories provided by prover */
+
+  private var loaded_theories: Set[String] = Set()
+
+  override def register_thy(thy_name: String)
+  {
+    synchronized { loaded_theories += thy_name }
+  }
+
+  override def is_loaded(thy_name: String): Boolean =
+    synchronized { loaded_theories.contains(thy_name) }
+
+
+  /* file-system operations */
+
+  override def append(master_dir: String, source_path: Path): String =
+  {
+    val path = source_path.expand
+    if (path.is_absolute) Isabelle_System.platform_path(path)
+    else {
+      val vfs = VFSManager.getVFSForPath(master_dir)
+      if (vfs.isInstanceOf[FileVFS])
+        MiscUtilities.resolveSymlinks(
+          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
+      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
+    }
+  }
+
+  override def check_thy(node_name: String): Thy_Header =
+  {
+    Swing_Thread.now {
+      Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
+        case Some(buffer) =>
+          Isabelle.buffer_lock(buffer) {
+            val text = new Segment
+            buffer.getText(0, buffer.getLength, text)
+            Some(Thy_Header.read(text))
+          }
+        case None => None
+      }
+    } getOrElse {
+      val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
+      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+      Thy_Header.read(file)
+    }
+  }
+}
+
diff -r f23ac1a679d1 -r 96b6388d06c4 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 22:10:08 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 11:43:47 2011 +0200
@@ -10,23 +10,20 @@
 import isabelle._
 
 import java.lang.System
-import java.io.{File, FileInputStream, IOException}
 import java.awt.Font
 import javax.swing.JOptionPane
-import javax.swing.text.Segment
 
 import scala.collection.mutable
 import scala.swing.ComboBox
 import scala.util.Sorting
 
 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
-  Buffer, EditPane, MiscUtilities, ServiceManager, View}
+  Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
-import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
 
 import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.util.Log
@@ -347,52 +344,9 @@
 
 class Plugin extends EBPlugin
 {
-  /* theory files via editor document model */
-
-  val thy_load = new Thy_Load
-  {
-    private var loaded_theories: Set[String] = Set()
-
-    def register_thy(thy_name: String)
-    {
-      synchronized { loaded_theories += thy_name }
-    }
-    def is_loaded(thy_name: String): Boolean =
-      synchronized { loaded_theories.contains(thy_name) }
+  /* theory files */
 
-    def append(master_dir: String, source_path: Path): String =
-    {
-      val path = source_path.expand
-      if (path.is_absolute) Isabelle_System.platform_path(path)
-      else {
-        val vfs = VFSManager.getVFSForPath(master_dir)
-        if (vfs.isInstanceOf[FileVFS])
-          MiscUtilities.resolveSymlinks(
-            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
-        else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
-      }
-    }
-
-    def check_thy(node_name: String): Thy_Header =
-    {
-      Swing_Thread.now {
-        Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
-          case Some(buffer) =>
-            Isabelle.buffer_lock(buffer) {
-              val text = new Segment
-              buffer.getText(0, buffer.getLength, text)
-              Some(Thy_Header.read(text))
-            }
-          case None => None
-        }
-      } getOrElse {
-        val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
-        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
-        Thy_Header.read(file)
-      }
-    }
-  }
-
+  val thy_load = new JEdit_Thy_Load
   val thy_info = new Thy_Info(thy_load)
 
   private lazy val delay_load =