merged
authorbulwahn
Sun Dec 16 19:13:19 2012 +0100 (2012-12-16)
changeset 505692019ca8dcbfa
parent 50568 ee090b5712f3
parent 50566 b43c4f660320
child 50570 fae8b1d9f701
merged
     1.1 --- a/src/Pure/General/symbol.scala	Sun Dec 16 18:12:18 2012 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Sun Dec 16 19:13:19 2012 +0100
     1.3 @@ -202,7 +202,7 @@
     1.4    /** symbol interpretation **/
     1.5  
     1.6    private lazy val symbols =
     1.7 -    new Interpretation(File.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS"))))
     1.8 +    new Interpretation(File.try_read(Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS"))))
     1.9  
    1.10    private class Interpretation(symbols_spec: String)
    1.11    {
     2.1 --- a/src/Pure/System/build.scala	Sun Dec 16 18:12:18 2012 +0100
     2.2 +++ b/src/Pure/System/build.scala	Sun Dec 16 19:13:19 2012 +0100
     2.3 @@ -370,7 +370,7 @@
     2.4            val thy_deps =
     2.5              thy_info.dependencies(inlined_files,
     2.6                info.theories.map(_._2).flatten.
     2.7 -                map(thy => Thy_Load.external_node(info.dir + Thy_Load.thy_path(thy))))
     2.8 +                map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
     2.9  
    2.10            val loaded_theories = thy_deps.loaded_theories
    2.11            val syntax = thy_deps.make_syntax
     3.1 --- a/src/Pure/System/session.scala	Sun Dec 16 18:12:18 2012 +0100
     3.2 +++ b/src/Pure/System/session.scala	Sun Dec 16 19:13:19 2012 +0100
     3.3 @@ -110,8 +110,8 @@
     3.4          case Text_Edits(previous, text_edits, version_result) =>
     3.5            val prev = previous.get_finished
     3.6            val (doc_edits, version) =
     3.7 -            Timing.timeit("Thy_Syntax.text_edits", timing) {
     3.8 -              Thy_Syntax.text_edits(thy_load.base_syntax, reparse_limit, prev, text_edits)
     3.9 +            Timing.timeit("Thy_Load.text_edits", timing) {
    3.10 +              thy_load.text_edits(reparse_limit, prev, text_edits)
    3.11              }
    3.12            version_result.fulfill(version)
    3.13            sender ! Change(doc_edits, prev, version)
     4.1 --- a/src/Pure/Thy/thy_load.scala	Sun Dec 16 18:12:18 2012 +0100
     4.2 +++ b/src/Pure/Thy/thy_load.scala	Sun Dec 16 19:13:19 2012 +0100
     4.3 @@ -23,9 +23,9 @@
     4.4      catch { case ERROR(_) => false }
     4.5  
     4.6  
     4.7 -  /* node names */
     4.8 +  /* document node names */
     4.9  
    4.10 -  def external_node(raw_path: Path): Document.Node.Name =
    4.11 +  def path_node_name(raw_path: Path): Document.Node.Name =
    4.12    {
    4.13      val path = raw_path.expand
    4.14      val node = path.implode
    4.15 @@ -122,5 +122,12 @@
    4.16  
    4.17    def check_thy(name: Document.Node.Name): Document.Node.Header =
    4.18      with_thy_text(name, check_thy_text(name, _))
    4.19 +
    4.20 +
    4.21 +  /* theory text edits */
    4.22 +
    4.23 +  def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
    4.24 +      : (List[Document.Edit_Command], Document.Version) =
    4.25 +    Thy_Syntax.text_edits(base_syntax, reparse_limit, previous, edits)
    4.26  }
    4.27  
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Dec 16 18:12:18 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Dec 16 19:13:19 2012 +0100
     5.3 @@ -23,7 +23,7 @@
     5.4  {
     5.5    /* document model of buffer */
     5.6  
     5.7 -  private val key = "isabelle.document_model"
     5.8 +  private val key = "PIDE.document_model"
     5.9  
    5.10    def apply(buffer: Buffer): Option[Document_Model] =
    5.11    {
     6.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Dec 16 18:12:18 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Dec 16 19:13:19 2012 +0100
     6.3 @@ -177,15 +177,15 @@
     6.4  
     6.5  
     6.6  class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
     6.7 -  "isabelle", PIDE.get_recent_syntax, JEdit_Lib.buffer_node_name)
     6.8 +  "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name)
     6.9  
    6.10  
    6.11  class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
    6.12 -  "isabelle-options", Some(Options.options_syntax), JEdit_Lib.buffer_node_dummy)
    6.13 +  "isabelle-options", Some(Options.options_syntax), PIDE.thy_load.buffer_node_dummy)
    6.14  
    6.15  
    6.16  class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
    6.17 -  "isabelle-root", Some(Build.root_syntax), JEdit_Lib.buffer_node_dummy)
    6.18 +  "isabelle-root", Some(Build.root_syntax), PIDE.thy_load.buffer_node_dummy)
    6.19  
    6.20  
    6.21  class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw", PIDE.get_recent_syntax)
     7.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Dec 16 18:12:18 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Dec 16 19:13:19 2012 +0100
     7.3 @@ -77,15 +77,6 @@
     7.4  
     7.5    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
     7.6  
     7.7 -  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
     7.8 -    Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
     7.9 -
    7.10 -  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
    7.11 -  {
    7.12 -    val name = buffer_name(buffer)
    7.13 -    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    7.14 -  }
    7.15 -
    7.16  
    7.17    /* main jEdit components */
    7.18  
     8.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Dec 16 18:12:18 2012 +0100
     8.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Dec 16 19:13:19 2012 +0100
     8.3 @@ -14,12 +14,26 @@
     8.4  
     8.5  import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
     8.6  import org.gjt.sp.jedit.MiscUtilities
     8.7 -import org.gjt.sp.jedit.View
     8.8 +import org.gjt.sp.jedit.{View, Buffer}
     8.9  
    8.10  
    8.11  class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
    8.12    extends Thy_Load(loaded_theories, base_syntax)
    8.13  {
    8.14 +  /* document node names */
    8.15 +
    8.16 +  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
    8.17 +    Some(Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName))
    8.18 +
    8.19 +  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
    8.20 +  {
    8.21 +    val name = JEdit_Lib.buffer_name(buffer)
    8.22 +    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    8.23 +  }
    8.24 +
    8.25 +
    8.26 +  /* file-system operations */
    8.27 +
    8.28    override def append(dir: String, source_path: Path): String =
    8.29    {
    8.30      val path = source_path.expand
     9.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Dec 16 18:12:18 2012 +0100
     9.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Dec 16 19:13:19 2012 +0100
     9.3 @@ -76,7 +76,7 @@
     9.4          (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
     9.5            JEdit_Lib.buffer_lock(buffer) {
     9.6              val (model_edits, opt_model) =
     9.7 -              JEdit_Lib.buffer_node_name(buffer) match {
     9.8 +              thy_load.buffer_node_name(buffer) match {
     9.9                  case Some(node_name) =>
    9.10                    document_model(buffer) match {
    9.11                      case Some(model) if model.name == node_name => (Nil, Some(model))
    9.12 @@ -95,7 +95,7 @@
    9.13              model_edits ::: edits
    9.14            }
    9.15          }
    9.16 -      PIDE.session.update(init_edits)
    9.17 +      session.update(init_edits)
    9.18      }
    9.19    }
    9.20  
    9.21 @@ -121,7 +121,7 @@
    9.22  
    9.23    def check_buffer(buffer: Buffer)
    9.24    {
    9.25 -    PIDE.document_model(buffer) match {
    9.26 +    document_model(buffer) match {
    9.27        case Some(model) => model.full_perspective()
    9.28        case None =>
    9.29      }