# HG changeset patch
# User bulwahn
# Date 1355681599 -3600
# Node ID 2019ca8dcbfa1ad0542b947aa2a8c489d82dcc45
# Parent  ee090b5712f32b4569ccb7c7ed92ac412a15d429# Parent  b43c4f660320f0e5e12bcd7604d0ea840d39ec81
merged

diff -r ee090b5712f3 -r 2019ca8dcbfa src/Pure/General/symbol.scala
--- 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)
   {
diff -r ee090b5712f3 -r 2019ca8dcbfa src/Pure/System/build.scala
--- 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
diff -r ee090b5712f3 -r 2019ca8dcbfa src/Pure/System/session.scala
--- 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)
diff -r ee090b5712f3 -r 2019ca8dcbfa src/Pure/Thy/thy_load.scala
--- 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)
 }
 
diff -r ee090b5712f3 -r 2019ca8dcbfa src/Tools/jEdit/src/document_model.scala
--- 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] =
   {
diff -r ee090b5712f3 -r 2019ca8dcbfa src/Tools/jEdit/src/isabelle_sidekick.scala
--- 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)
diff -r ee090b5712f3 -r 2019ca8dcbfa src/Tools/jEdit/src/jedit_lib.scala
--- 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 */
 
diff -r ee090b5712f3 -r 2019ca8dcbfa src/Tools/jEdit/src/jedit_thy_load.scala
--- 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
diff -r ee090b5712f3 -r 2019ca8dcbfa src/Tools/jEdit/src/plugin.scala
--- 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 =>
     }