src/Tools/jEdit/src/jedit_resources.scala
author wenzelm
Fri, 21 Apr 2017 14:09:03 +0200
changeset 65532 febfd9f78bd4
parent 65524 0910f1733909
child 66195 bb886f13623a
permissions -rw-r--r--
eliminated default_qualifier: just a constant;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56208
06cc31dff138 clarifed module name;
wenzelm
parents: 55134
diff changeset
     1
/*  Title:      Tools/jEdit/src/jedit_resources.scala
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
     3
56208
06cc31dff138 clarifed module name;
wenzelm
parents: 55134
diff changeset
     4
Resources for theories and auxiliary files, based on jEdit buffer
06cc31dff138 clarifed module name;
wenzelm
parents: 55134
diff changeset
     5
content and virtual file-systems.
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
     6
*/
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
     7
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
     8
package isabelle.jedit
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
     9
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    10
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    11
import isabelle._
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    12
56502
db2836f65d42 improved support for external URLs, based on standard Java network operations;
wenzelm
parents: 56460
diff changeset
    13
import java.io.{File => JFile, ByteArrayOutputStream}
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    14
import javax.swing.text.Segment
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    15
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
    16
import scala.util.parsing.input.Reader
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
    17
56502
db2836f65d42 improved support for external URLs, based on standard Java network operations;
wenzelm
parents: 56460
diff changeset
    18
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    19
import org.gjt.sp.jedit.MiscUtilities
55134
1b67b17cdad5 propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents: 54517
diff changeset
    20
import org.gjt.sp.jedit.{jEdit, View, Buffer}
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
    21
import org.gjt.sp.jedit.bufferio.BufferIORequest
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    22
56208
06cc31dff138 clarifed module name;
wenzelm
parents: 55134
diff changeset
    23
65441
9425e4d8bdb6 more session_base information in ML;
wenzelm
parents: 65361
diff changeset
    24
class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    25
{
64834
wenzelm
parents: 64813
diff changeset
    26
  /* document node name */
50566
b43c4f660320 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents: 49406
diff changeset
    27
65501
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    28
  def known_file(path: String): Option[Document.Node.Name] =
65524
0910f1733909 tuned signature;
wenzelm
parents: 65501
diff changeset
    29
    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
65501
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    30
64841
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    31
  def node_name(path: String): Document.Node.Name =
65501
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    32
    known_file(path) getOrElse {
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    33
      val vfs = VFSManager.getVFSForPath(path)
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    34
      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
65532
febfd9f78bd4 eliminated default_qualifier: just a constant;
wenzelm
parents: 65524
diff changeset
    35
      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
65501
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    36
        case (true, theory) => Document.Node.Name.loaded_theory(theory)
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    37
        case (false, theory) =>
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    38
          val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    39
          Document.Node.Name(node, master_dir, theory)
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    40
      }
65472
wenzelm
parents: 65471
diff changeset
    41
    }
64841
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    42
65469
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 65452
diff changeset
    43
  def node_name(buffer: Buffer): Document.Node.Name =
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 65452
diff changeset
    44
    node_name(JEdit_Lib.buffer_name(buffer))
64858
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64856
diff changeset
    45
54509
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 50566
diff changeset
    46
  def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 50566
diff changeset
    47
  {
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 50566
diff changeset
    48
    val name = node_name(buffer)
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 50566
diff changeset
    49
    if (name.is_theory) Some(name) else None
50566
b43c4f660320 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents: 49406
diff changeset
    50
  }
b43c4f660320 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents: 49406
diff changeset
    51
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44580
diff changeset
    52
  override def append(dir: String, source_path: Path): String =
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    53
  {
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    54
    val path = source_path.expand
57841
e212e2001b2a always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;
wenzelm
parents: 57622
diff changeset
    55
    if (dir == "" || path.is_absolute)
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 60917
diff changeset
    56
      MiscUtilities.resolveSymlinks(File.platform_path(path))
56502
db2836f65d42 improved support for external URLs, based on standard Java network operations;
wenzelm
parents: 56460
diff changeset
    57
    else if (path.is_current) dir
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    58
    else {
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44580
diff changeset
    59
      val vfs = VFSManager.getVFSForPath(dir)
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    60
      if (vfs.isInstanceOf[FileVFS])
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    61
        MiscUtilities.resolveSymlinks(
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 60917
diff changeset
    62
          vfs.constructPath(dir, File.platform_path(path)))
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 60917
diff changeset
    63
      else vfs.constructPath(dir, File.standard_path(path))
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    64
    }
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    65
  }
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
    66
64834
wenzelm
parents: 64813
diff changeset
    67
wenzelm
parents: 64813
diff changeset
    68
  /* file content */
wenzelm
parents: 64813
diff changeset
    69
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    70
  def read_file_content(node_name: Document.Node.Name): Option[String] =
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    71
  {
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    72
    val name = node_name.node
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    73
    try {
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    74
      val text =
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    75
        if (Url.is_wellformed(name)) Url.read(Url(name))
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    76
        else File.read(new JFile(name))
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    77
      Some(Symbol.decode(Line.normalize(text)))
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    78
    }
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    79
    catch { case ERROR(_) => None }
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    80
  }
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
    81
64841
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    82
  def get_file_content(node_name: Document.Node.Name): Option[String] =
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    83
    Document_Model.get(node_name) match {
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    84
      case Some(model: Buffer_Model) => Some(JEdit_Lib.buffer_text(model.buffer))
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    85
      case Some(model: File_Model) => Some(model.content.text)
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    86
      case None => read_file_content(node_name)
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    87
    }
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    88
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
    89
  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
48885
d5fdaf7dd1f8 find files via load commands within theory text;
wenzelm
parents: 48883
diff changeset
    90
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56823
diff changeset
    91
    GUI_Thread.now {
64837
4efe34df9136 refer to internal File_Model instead of external file;
wenzelm
parents: 64836
diff changeset
    92
      Document_Model.get(name) match {
64841
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    93
        case Some(model: Buffer_Model) =>
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    94
          JEdit_Lib.buffer_lock(model.buffer) { Some(f(JEdit_Lib.buffer_reader(model.buffer))) }
d53696aed874 added node_name(String): imitate jEdit buffer operations;
wenzelm
parents: 64837
diff changeset
    95
        case Some(model: File_Model) => Some(f(Scan.char_reader(model.content.text)))
48885
d5fdaf7dd1f8 find files via load commands within theory text;
wenzelm
parents: 48883
diff changeset
    96
        case None => None
d5fdaf7dd1f8 find files via load commands within theory text;
wenzelm
parents: 48883
diff changeset
    97
      }
d5fdaf7dd1f8 find files via load commands within theory text;
wenzelm
parents: 48883
diff changeset
    98
    } getOrElse {
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
    99
      if (Url.is_wellformed(name.node)) f(Scan.byte_reader(Url(name.node)))
56502
db2836f65d42 improved support for external URLs, based on standard Java network operations;
wenzelm
parents: 56460
diff changeset
   100
      else {
db2836f65d42 improved support for external URLs, based on standard Java network operations;
wenzelm
parents: 56460
diff changeset
   101
        val file = new JFile(name.node)
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   102
        if (file.isFile) f(Scan.byte_reader(file))
56502
db2836f65d42 improved support for external URLs, based on standard Java network operations;
wenzelm
parents: 56460
diff changeset
   103
        else error("No such file: " + quote(file.toString))
db2836f65d42 improved support for external URLs, based on standard Java network operations;
wenzelm
parents: 56460
diff changeset
   104
      }
48885
d5fdaf7dd1f8 find files via load commands within theory text;
wenzelm
parents: 48883
diff changeset
   105
    }
d5fdaf7dd1f8 find files via load commands within theory text;
wenzelm
parents: 48883
diff changeset
   106
  }
d5fdaf7dd1f8 find files via load commands within theory text;
wenzelm
parents: 48883
diff changeset
   107
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   108
56666
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   109
  private class File_Content_Output(buffer: Buffer) extends
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   110
    ByteArrayOutputStream(buffer.getLength + 1)
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   111
  {
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   112
    def content(): Bytes = Bytes(this.buf, 0, this.count)
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   113
  }
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   114
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   115
  private class File_Content(buffer: Buffer) extends
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   116
    BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath)
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   117
  {
56666
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   118
    def _run() { }
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   119
    def content(): Bytes =
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   120
    {
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   121
      val out = new File_Content_Output(buffer)
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   122
      write(buffer, out)
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   123
      out.content()
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   124
    }
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   125
  }
55134
1b67b17cdad5 propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents: 54517
diff changeset
   126
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64834
diff changeset
   127
  def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
56666
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56502
diff changeset
   128
55134
1b67b17cdad5 propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents: 54517
diff changeset
   129
1b67b17cdad5 propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents: 54517
diff changeset
   130
  /* theory text edits */
1b67b17cdad5 propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents: 54517
diff changeset
   131
56316
b1cf8ddc2e04 propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents: 56208
diff changeset
   132
  override def commit(change: Session.Change)
b1cf8ddc2e04 propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents: 56208
diff changeset
   133
  {
59319
wenzelm
parents: 59078
diff changeset
   134
    if (change.syntax_changed.nonEmpty)
64836
wenzelm
parents: 64835
diff changeset
   135
      GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
60917
0607869c2ff3 more thorough reload;
wenzelm
parents: 60916
diff changeset
   136
    if (change.deps_changed ||
61023
46df28442a80 clarified undefined_blobs: already loaded theories are suppressed;
wenzelm
parents: 60988
diff changeset
   137
        PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
65243
ba5ce07e06a7 proper plugin access;
wenzelm
parents: 64858
diff changeset
   138
      PIDE.plugin.deps_changed()
56316
b1cf8ddc2e04 propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents: 56208
diff changeset
   139
  }
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff changeset
   140
}