src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Fri, 30 Jun 2017 14:26:45 +0200
changeset 66235 d4fa51e7c4ff
parent 66234 836898197296
child 66674 30d5195299e2
permissions -rw-r--r--
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64605
diff changeset
     1
/*  Title:      Tools/VSCode/src/vscode_resources.scala
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     3
64729
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 64727
diff changeset
     4
Resources for VSCode Language Server: file-system access and global state.
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     5
*/
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     6
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     7
package isabelle.vscode
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     8
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     9
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    10
import isabelle._
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    11
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    12
import java.io.{File => JFile}
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    13
64824
330ec9bc4b75 tuned signature;
wenzelm
parents: 64821
diff changeset
    14
import scala.util.parsing.input.Reader
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
    15
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    16
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64605
diff changeset
    17
object VSCode_Resources
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    18
{
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    19
  /* internal state */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    20
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    21
  sealed case class State(
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    22
    models: Map[JFile, Document_Model] = Map.empty,
65926
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    23
    caret: Option[(JFile, Line.Position)] = None,
66101
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    24
    overlays: Document.Overlays = Document.Overlays.empty,
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    25
    pending_input: Set[JFile] = Set.empty,
65926
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    26
    pending_output: Set[JFile] = Set.empty)
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    27
  {
65113
wenzelm
parents: 65112
diff changeset
    28
    def update_models(changed: Traversable[(JFile, Document_Model)]): State =
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
    29
      copy(
65113
wenzelm
parents: 65112
diff changeset
    30
        models = models ++ changed,
wenzelm
parents: 65112
diff changeset
    31
        pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
wenzelm
parents: 65112
diff changeset
    32
        pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file })
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
    33
65926
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    34
    def update_caret(new_caret: Option[(JFile, Line.Position)]): State =
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    35
      if (caret == new_caret) this
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    36
      else
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    37
        copy(
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    38
          caret = new_caret,
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    39
          pending_input = pending_input ++ caret.map(_._1) ++ new_caret.map(_._1))
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    40
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    41
    def get_caret(file: JFile): Option[Line.Position] =
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    42
      caret match {
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    43
        case Some((caret_file, caret_pos)) if caret_file == file => Some(caret_pos)
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    44
        case _ => None
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    45
      }
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
    46
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    47
    lazy val document_blobs: Document.Blobs =
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    48
      Document.Blobs(
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    49
        (for {
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    50
          (_, model) <- models.iterator
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    51
          blob <- model.get_blob
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    52
        } yield (model.node_name -> blob)).toMap)
66101
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    53
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    54
    def change_overlay(insert: Boolean, file: JFile,
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    55
        command: Command, fn: String, args: List[String]): State =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    56
      copy(
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    57
        overlays =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    58
          if (insert) overlays.insert(command, fn, args)
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    59
          else overlays.remove(command, fn, args),
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
    60
        pending_input = pending_input + file)
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    61
  }
66086
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
    62
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
    63
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
    64
  /* caret */
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
    65
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
    66
  sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset)
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
    67
  {
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
    68
    def node_name: Document.Node.Name = model.node_name
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
    69
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    70
}
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    71
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64605
diff changeset
    72
class VSCode_Resources(
65361
ecefb68dc21d tuned signature;
wenzelm
parents: 65359
diff changeset
    73
    val options: Options,
ecefb68dc21d tuned signature;
wenzelm
parents: 65359
diff changeset
    74
    session_base: Sessions.Base,
ecefb68dc21d tuned signature;
wenzelm
parents: 65359
diff changeset
    75
    log: Logger = No_Logger)
65441
9425e4d8bdb6 more session_base information in ML;
wenzelm
parents: 65361
diff changeset
    76
  extends Resources(session_base, log = log)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    77
{
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    78
  private val state = Synchronized(VSCode_Resources.State())
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    79
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    80
65137
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    81
  /* options */
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    82
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    83
  def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    84
  def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    85
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    86
  def message_margin: Int = options.int("vscode_message_margin")
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    87
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    88
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    89
  /* document node name */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    90
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    91
  def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    92
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    93
  def node_name(file: JFile): Document.Node.Name =
66195
bb886f13623a proper bootstrap_name (amending b42743f5b595);
wenzelm
parents: 66152
diff changeset
    94
    session_base.known.get_file(file, bootstrap = true) getOrElse {
65501
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    95
      val node = file.getPath
65532
febfd9f78bd4 eliminated default_qualifier: just a constant;
wenzelm
parents: 65524
diff changeset
    96
      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
    97
        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
    98
        case (false, theory) =>
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
    99
          val master_dir = if (theory == "") "" else file.getParent
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
   100
          Document.Node.Name(node, master_dir, theory)
b42743f5b595 prefer formal name from session context, for proper qualified theory name;
wenzelm
parents: 65476
diff changeset
   101
      }
65472
wenzelm
parents: 65471
diff changeset
   102
    }
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   103
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
   104
  override def append(dir: String, source_path: Path): String =
64716
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
   105
  {
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
   106
    val path = source_path.expand
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   107
    if (dir == "" || path.is_absolute) File.platform_path(path)
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
   108
    else if (path.is_current) dir
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   109
    else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   110
      dir + JFile.separator + File.platform_path(path)
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   111
    else if (path.is_basic) dir + File.platform_path(path)
66235
d4fa51e7c4ff retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
wenzelm
parents: 66234
diff changeset
   112
    else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
64716
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
   113
  }
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
   114
66152
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   115
  def get_models: Map[JFile, Document_Model] = state.value.models
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   116
  def get_model(file: JFile): Option[Document_Model] = get_models.get(file)
64834
wenzelm
parents: 64833
diff changeset
   117
  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
wenzelm
parents: 64833
diff changeset
   118
wenzelm
parents: 64833
diff changeset
   119
wenzelm
parents: 64833
diff changeset
   120
  /* file content */
wenzelm
parents: 64833
diff changeset
   121
wenzelm
parents: 64833
diff changeset
   122
  def read_file_content(file: JFile): Option[String] =
wenzelm
parents: 64833
diff changeset
   123
    try { Some(Line.normalize(File.read(file))) }
wenzelm
parents: 64833
diff changeset
   124
    catch { case ERROR(_) => None }
wenzelm
parents: 64833
diff changeset
   125
wenzelm
parents: 64833
diff changeset
   126
  def get_file_content(file: JFile): Option[String] =
wenzelm
parents: 64833
diff changeset
   127
    get_model(file) match {
wenzelm
parents: 64833
diff changeset
   128
      case Some(model) => Some(model.content.text)
wenzelm
parents: 64833
diff changeset
   129
      case None => read_file_content(file)
wenzelm
parents: 64833
diff changeset
   130
    }
wenzelm
parents: 64833
diff changeset
   131
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   132
  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   133
  {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   134
    val file = node_file(name)
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   135
    get_model(file) match {
64830
9bc44bef99e6 more explocit Document_Model.Content;
wenzelm
parents: 64824
diff changeset
   136
      case Some(model) => f(Scan.char_reader(model.content.text))
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   137
      case None if file.isFile =>
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   138
        val reader = Scan.byte_reader(file)
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   139
        try { f(reader) } finally { reader.close }
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   140
      case None =>
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   141
        error("No such file: " + quote(file.toString))
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   142
    }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   143
  }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   144
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   145
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   146
  /* document models */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   147
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   148
  def visible_node(name: Document.Node.Name): Boolean =
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   149
    get_model(name) match {
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   150
      case Some(model) => model.node_visible
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   151
      case None => false
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   152
    }
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   153
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   154
  def change_model(
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   155
    session: Session,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   156
    editor: Server.Editor,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   157
    file: JFile,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   158
    text: String,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   159
    range: Option[Line.Range] = None)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   160
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   161
    state.change(st =>
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
   162
      {
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   163
        val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
65160
6e042537555d incremental document changes;
wenzelm
parents: 65142
diff changeset
   164
        val model1 = (model.change_text(text, range) getOrElse model).external(false)
65114
200b787ceb51 potentially redundant pending_output, for the sake of uniformity and reactivity;
wenzelm
parents: 65113
diff changeset
   165
        st.update_models(Some(file -> model1))
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
   166
      })
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   167
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   168
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   169
  def close_model(file: JFile): Boolean =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   170
    state.change_result(st =>
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   171
      st.models.get(file) match {
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   172
        case None => (false, st)
65113
wenzelm
parents: 65112
diff changeset
   173
        case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   174
      })
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   175
65116
06d9bcb66ef3 simplified;
wenzelm
parents: 65115
diff changeset
   176
  def sync_models(changed_files: Set[JFile]): Unit =
06d9bcb66ef3 simplified;
wenzelm
parents: 65115
diff changeset
   177
    state.change(st =>
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   178
      {
64719
wenzelm
parents: 64718
diff changeset
   179
        val changed_models =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   180
          (for {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   181
            (file, model) <- st.models.iterator
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   182
            if changed_files(file) && model.external_file
64812
ddbb89e7621d tuned signature;
wenzelm
parents: 64806
diff changeset
   183
            text <- read_file_content(file)
65160
6e042537555d incremental document changes;
wenzelm
parents: 65142
diff changeset
   184
            model1 <- model.change_text(text)
65116
06d9bcb66ef3 simplified;
wenzelm
parents: 65115
diff changeset
   185
          } yield (file, model1)).toList
06d9bcb66ef3 simplified;
wenzelm
parents: 65115
diff changeset
   186
        st.update_models(changed_models)
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   187
      })
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   188
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   189
66101
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   190
  /* overlays */
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   191
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   192
  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   193
    state.value.overlays(name)
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   194
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   195
  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   196
    state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args))
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   197
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   198
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   199
    state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args))
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   200
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   201
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   202
  /* resolve dependencies */
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   203
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   204
  def resolve_dependencies(
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   205
    session: Session,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   206
    editor: Server.Editor,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   207
    file_watcher: File_Watcher): (Boolean, Boolean) =
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   208
  {
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   209
    state.change_result(st =>
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   210
      {
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   211
        /* theory files */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   212
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   213
        val thys =
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   214
          (for ((_, model) <- st.models.iterator if model.is_theory)
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   215
           yield (model.node_name, Position.none)).toList
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   216
65359
9ca34f0407a9 provide session qualifier via resources;
wenzelm
parents: 65232
diff changeset
   217
        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   218
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   219
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   220
        /* auxiliary files */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   221
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   222
        val stable_tip_version =
64815
wenzelm
parents: 64812
diff changeset
   223
          if (st.models.forall(entry => entry._2.is_stable))
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   224
            session.current_state().stable_tip_version
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   225
          else None
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   226
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   227
        val aux_files =
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   228
          stable_tip_version match {
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   229
            case Some(version) => undefined_blobs(version.nodes)
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   230
            case None => Nil
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   231
          }
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   232
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   233
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   234
        /* loaded models */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   235
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   236
        val loaded_models =
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   237
          (for {
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   238
            node_name <- thy_files.iterator ++ aux_files.iterator
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   239
            file = node_file(node_name)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   240
            if !st.models.isDefinedAt(file)
64857
wenzelm
parents: 64856
diff changeset
   241
            text <- { file_watcher.register_parent(file); read_file_content(file) }
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   242
          }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   243
          yield {
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   244
            val model = Document_Model.init(session, editor, node_name)
65160
6e042537555d incremental document changes;
wenzelm
parents: 65142
diff changeset
   245
            val model1 = (model.change_text(text) getOrElse model).external(true)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   246
            (file, model1)
65117
wenzelm
parents: 65116
diff changeset
   247
          }).toList
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   248
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   249
        val invoke_input = loaded_models.nonEmpty
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   250
        val invoke_load = stable_tip_version.isEmpty
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   251
65113
wenzelm
parents: 65112
diff changeset
   252
        ((invoke_input, invoke_load), st.update_models(loaded_models))
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   253
      })
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   254
  }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   255
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   256
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   257
  /* pending input */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   258
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   259
  def flush_input(session: Session)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   260
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   261
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   262
      {
64719
wenzelm
parents: 64718
diff changeset
   263
        val changed_models =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   264
          (for {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   265
            file <- st.pending_input.iterator
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   266
            model <- st.models.get(file)
65926
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
   267
            (edits, model1) <- model.flush_edits(st.document_blobs, st.get_caret(file))
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   268
          } yield (edits, (file, model1))).toList
64707
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
   269
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   270
        session.update(st.document_blobs, changed_models.flatMap(_._1))
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   271
        st.copy(
65112
wenzelm
parents: 65111
diff changeset
   272
          models = st.models ++ changed_models.iterator.map(_._2),
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   273
          pending_input = Set.empty)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   274
      })
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   275
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   276
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   277
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   278
  /* pending output */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   279
65118
31fd8e41be02 tuned signature;
wenzelm
parents: 65117
diff changeset
   280
  def update_output(changed_nodes: Traversable[JFile]): Unit =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   281
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   282
66138
f7ef4c50b747 added commands for spell-checker dictionary;
wenzelm
parents: 66101
diff changeset
   283
  def update_output_visible(): Unit =
f7ef4c50b747 added commands for spell-checker dictionary;
wenzelm
parents: 66101
diff changeset
   284
    state.change(st => st.copy(pending_output = st.pending_output ++
f7ef4c50b747 added commands for spell-checker dictionary;
wenzelm
parents: 66101
diff changeset
   285
      (for ((file, model) <- st.models.iterator if model.node_visible) yield file)))
f7ef4c50b747 added commands for spell-checker dictionary;
wenzelm
parents: 66101
diff changeset
   286
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   287
  def flush_output(channel: Channel): Boolean =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   288
  {
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   289
    state.change_result(st =>
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   290
      {
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   291
        val (postponed, flushed) =
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   292
          (for {
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   293
            file <- st.pending_output.iterator
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   294
            model <- st.models.get(file)
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   295
          } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   296
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   297
        val changed_iterator =
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   298
          for {
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   299
            (file, model, rendering) <- flushed.iterator
65115
93a0683e075a publish output more thoroughly;
wenzelm
parents: 65114
diff changeset
   300
            (changed_diags, changed_decos, model1) = model.publish(rendering)
93a0683e075a publish output more thoroughly;
wenzelm
parents: 65114
diff changeset
   301
            if changed_diags.isDefined || changed_decos.isDefined
65095
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   302
          }
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   303
          yield {
65115
93a0683e075a publish output more thoroughly;
wenzelm
parents: 65114
diff changeset
   304
            for (diags <- changed_diags)
93a0683e075a publish output more thoroughly;
wenzelm
parents: 65114
diff changeset
   305
              channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
65137
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   306
            if (pide_extensions) {
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   307
              for (decos <- changed_decos; deco <- decos)
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   308
                channel.write(rendering.decoration_output(deco).json(file))
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   309
            }
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   310
            (file, model1)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   311
          }
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   312
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   313
        (postponed.nonEmpty,
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   314
          st.copy(
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   315
            models = st.models ++ changed_iterator,
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   316
            pending_output = postponed.map(_._1).toSet))
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   317
      }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   318
    )
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   319
  }
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   320
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   321
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   322
  /* output text */
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   323
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   324
  def output_text(s: String): String =
65137
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   325
    if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   326
65107
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   327
  def output_xml(xml: XML.Tree): String =
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   328
    output_text(XML.content(xml))
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   329
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   330
  def output_pretty(body: XML.Body, margin: Int): String =
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   331
    output_text(Pretty.string_of(body, margin))
65107
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   332
  def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   333
  def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   334
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   335
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   336
  /* caret handling */
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   337
65191
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
   338
  def update_caret(caret: Option[(JFile, Line.Position)])
65926
0f7821a07aa9 restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents: 65532
diff changeset
   339
  { state.change(_.update_caret(caret)) }
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   340
66086
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
   341
  def get_caret(): Option[VSCode_Resources.Caret] =
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   342
  {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   343
    val st = state.value
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   344
    for {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   345
      (file, pos) <- st.caret
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   346
      model <- st.models.get(file)
65191
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
   347
      offset <- model.content.doc.offset(pos)
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   348
    }
66086
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
   349
    yield VSCode_Resources.Caret(file, model, offset)
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   350
  }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   351
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   352
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   353
  /* spell checker */
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   354
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   355
  val spell_checker = new Spell_Checker_Variable
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   356
  spell_checker.update(options)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   357
}