--- a/src/Pure/General/symbol.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Pure/General/symbol.scala Sun Dec 16 19:13:19 2012 +0100
@@ -202,7 +202,7 @@
/** symbol interpretation **/
private lazy val symbols =
- new Interpretation(File.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS"))))
+ new Interpretation(File.try_read(Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS"))))
private class Interpretation(symbols_spec: String)
{
--- a/src/Pure/System/build.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Pure/System/build.scala Sun Dec 16 19:13:19 2012 +0100
@@ -370,7 +370,7 @@
val thy_deps =
thy_info.dependencies(inlined_files,
info.theories.map(_._2).flatten.
- map(thy => Thy_Load.external_node(info.dir + Thy_Load.thy_path(thy))))
+ map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
val loaded_theories = thy_deps.loaded_theories
val syntax = thy_deps.make_syntax
--- a/src/Pure/System/session.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Pure/System/session.scala Sun Dec 16 19:13:19 2012 +0100
@@ -110,8 +110,8 @@
case Text_Edits(previous, text_edits, version_result) =>
val prev = previous.get_finished
val (doc_edits, version) =
- Timing.timeit("Thy_Syntax.text_edits", timing) {
- Thy_Syntax.text_edits(thy_load.base_syntax, reparse_limit, prev, text_edits)
+ Timing.timeit("Thy_Load.text_edits", timing) {
+ thy_load.text_edits(reparse_limit, prev, text_edits)
}
version_result.fulfill(version)
sender ! Change(doc_edits, prev, version)
--- a/src/Pure/Thy/thy_load.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala Sun Dec 16 19:13:19 2012 +0100
@@ -23,9 +23,9 @@
catch { case ERROR(_) => false }
- /* node names */
+ /* document node names */
- def external_node(raw_path: Path): Document.Node.Name =
+ def path_node_name(raw_path: Path): Document.Node.Name =
{
val path = raw_path.expand
val node = path.implode
@@ -122,5 +122,12 @@
def check_thy(name: Document.Node.Name): Document.Node.Header =
with_thy_text(name, check_thy_text(name, _))
+
+
+ /* theory text edits */
+
+ def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
+ : (List[Document.Edit_Command], Document.Version) =
+ Thy_Syntax.text_edits(base_syntax, reparse_limit, previous, edits)
}
--- a/src/Tools/jEdit/src/document_model.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Dec 16 19:13:19 2012 +0100
@@ -23,7 +23,7 @@
{
/* document model of buffer */
- private val key = "isabelle.document_model"
+ private val key = "PIDE.document_model"
def apply(buffer: Buffer): Option[Document_Model] =
{
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Dec 16 19:13:19 2012 +0100
@@ -177,15 +177,15 @@
class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
- "isabelle", PIDE.get_recent_syntax, JEdit_Lib.buffer_node_name)
+ "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name)
class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
- "isabelle-options", Some(Options.options_syntax), JEdit_Lib.buffer_node_dummy)
+ "isabelle-options", Some(Options.options_syntax), PIDE.thy_load.buffer_node_dummy)
class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
- "isabelle-root", Some(Build.root_syntax), JEdit_Lib.buffer_node_dummy)
+ "isabelle-root", Some(Build.root_syntax), PIDE.thy_load.buffer_node_dummy)
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw", PIDE.get_recent_syntax)
--- a/src/Tools/jEdit/src/jedit_lib.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Dec 16 19:13:19 2012 +0100
@@ -77,15 +77,6 @@
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
- def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
- Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
-
- def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
- {
- val name = buffer_name(buffer)
- Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
- }
-
/* main jEdit components */
--- a/src/Tools/jEdit/src/jedit_thy_load.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Sun Dec 16 19:13:19 2012 +0100
@@ -14,12 +14,26 @@
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
import org.gjt.sp.jedit.MiscUtilities
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{View, Buffer}
class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
extends Thy_Load(loaded_theories, base_syntax)
{
+ /* document node names */
+
+ def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
+ Some(Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName))
+
+ def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+ {
+ val name = JEdit_Lib.buffer_name(buffer)
+ Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+ }
+
+
+ /* file-system operations */
+
override def append(dir: String, source_path: Path): String =
{
val path = source_path.expand
--- a/src/Tools/jEdit/src/plugin.scala Sun Dec 16 18:12:18 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Dec 16 19:13:19 2012 +0100
@@ -76,7 +76,7 @@
(List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
JEdit_Lib.buffer_lock(buffer) {
val (model_edits, opt_model) =
- JEdit_Lib.buffer_node_name(buffer) match {
+ thy_load.buffer_node_name(buffer) match {
case Some(node_name) =>
document_model(buffer) match {
case Some(model) if model.name == node_name => (Nil, Some(model))
@@ -95,7 +95,7 @@
model_edits ::: edits
}
}
- PIDE.session.update(init_edits)
+ session.update(init_edits)
}
}
@@ -121,7 +121,7 @@
def check_buffer(buffer: Buffer)
{
- PIDE.document_model(buffer) match {
+ document_model(buffer) match {
case Some(model) => model.full_perspective()
case None =>
}