src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Wed, 07 Nov 2018 21:42:16 +0100
changeset 69255 800b1ce96fce
parent 67547 aefe7a7b330a
child 69256 c78c95d2a3d1
permissions -rw-r--r--
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
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
{
67292
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
    78
  resources =>
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
    79
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    80
  private val state = Synchronized(VSCode_Resources.State())
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    81
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    82
65137
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    83
  /* options */
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    84
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    85
  def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    86
  def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    87
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    88
  def message_margin: Int = options.int("vscode_message_margin")
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    89
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
    90
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    91
  /* document node name */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    92
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    93
  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
    94
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    95
  def node_name(file: JFile): Document.Node.Name =
67060
9ad7bf553ee1 tuned signature (again, see 1a9e2a2bf251);
wenzelm
parents: 67059
diff changeset
    96
    session_base.known.get_file(file, bootstrap = true) getOrElse {
9ad7bf553ee1 tuned signature (again, see 1a9e2a2bf251);
wenzelm
parents: 67059
diff changeset
    97
      val node = file.getPath
67104
a2fa0c6a7aff clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents: 67060
diff changeset
    98
      val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
a2fa0c6a7aff clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents: 67060
diff changeset
    99
      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
a2fa0c6a7aff clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents: 67060
diff changeset
   100
      else {
67292
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   101
        val master_dir = file.getParent
67104
a2fa0c6a7aff clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents: 67060
diff changeset
   102
        Document.Node.Name(node, master_dir, theory)
67060
9ad7bf553ee1 tuned signature (again, see 1a9e2a2bf251);
wenzelm
parents: 67059
diff changeset
   103
      }
9ad7bf553ee1 tuned signature (again, see 1a9e2a2bf251);
wenzelm
parents: 67059
diff changeset
   104
    }
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   105
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
   106
  override def append(dir: String, source_path: Path): String =
64716
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
   107
  {
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
   108
    val path = source_path.expand
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   109
    if (dir == "" || path.is_absolute) File.platform_path(path)
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
   110
    else if (path.is_current) dir
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   111
    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
   112
      dir + JFile.separator + File.platform_path(path)
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   113
    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
   114
    else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
64716
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
   115
  }
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
   116
66152
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   117
  def get_models: Map[JFile, Document_Model] = state.value.models
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   118
  def get_model(file: JFile): Option[Document_Model] = get_models.get(file)
64834
wenzelm
parents: 64833
diff changeset
   119
  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
wenzelm
parents: 64833
diff changeset
   120
wenzelm
parents: 64833
diff changeset
   121
wenzelm
parents: 64833
diff changeset
   122
  /* file content */
wenzelm
parents: 64833
diff changeset
   123
wenzelm
parents: 64833
diff changeset
   124
  def read_file_content(file: JFile): Option[String] =
67292
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   125
  {
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 67547
diff changeset
   126
    try { Some(Line.normalize(File.read(file))) }
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 67547
diff changeset
   127
    catch { case ERROR(_) => None }
67292
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   128
  }
64834
wenzelm
parents: 64833
diff changeset
   129
wenzelm
parents: 64833
diff changeset
   130
  def get_file_content(file: JFile): Option[String] =
wenzelm
parents: 64833
diff changeset
   131
    get_model(file) match {
wenzelm
parents: 64833
diff changeset
   132
      case Some(model) => Some(model.content.text)
wenzelm
parents: 64833
diff changeset
   133
      case None => read_file_content(file)
wenzelm
parents: 64833
diff changeset
   134
    }
wenzelm
parents: 64833
diff changeset
   135
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   136
  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
   137
  {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   138
    val file = node_file(name)
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   139
    get_model(file) match {
64830
9bc44bef99e6 more explocit Document_Model.Content;
wenzelm
parents: 64824
diff changeset
   140
      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
   141
      case None if file.isFile =>
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   142
        val reader = Scan.byte_reader(file)
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   143
        try { f(reader) } finally { reader.close }
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   144
      case None =>
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   145
        error("No such file: " + quote(file.toString))
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   146
    }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   147
  }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   148
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   149
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   150
  /* document models */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   151
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   152
  def visible_node(name: Document.Node.Name): Boolean =
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   153
    get_model(name) match {
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   154
      case Some(model) => model.node_visible
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   155
      case None => false
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   156
    }
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   157
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   158
  def change_model(
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   159
    session: Session,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   160
    editor: Server.Editor,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   161
    file: JFile,
66674
30d5195299e2 store document version;
wenzelm
parents: 66235
diff changeset
   162
    version: Long,
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   163
    text: String,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   164
    range: Option[Line.Range] = None)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   165
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   166
    state.change(st =>
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
   167
      {
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   168
        val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
66674
30d5195299e2 store document version;
wenzelm
parents: 66235
diff changeset
   169
        val model1 =
30d5195299e2 store document version;
wenzelm
parents: 66235
diff changeset
   170
          (model.change_text(text, range) getOrElse model).set_version(version).external(false)
65114
200b787ceb51 potentially redundant pending_output, for the sake of uniformity and reactivity;
wenzelm
parents: 65113
diff changeset
   171
        st.update_models(Some(file -> model1))
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
   172
      })
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   173
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   174
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   175
  def close_model(file: JFile): Boolean =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   176
    state.change_result(st =>
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   177
      st.models.get(file) match {
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   178
        case None => (false, st)
65113
wenzelm
parents: 65112
diff changeset
   179
        case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   180
      })
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   181
65116
06d9bcb66ef3 simplified;
wenzelm
parents: 65115
diff changeset
   182
  def sync_models(changed_files: Set[JFile]): Unit =
06d9bcb66ef3 simplified;
wenzelm
parents: 65115
diff changeset
   183
    state.change(st =>
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   184
      {
64719
wenzelm
parents: 64718
diff changeset
   185
        val changed_models =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   186
          (for {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   187
            (file, model) <- st.models.iterator
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   188
            if changed_files(file) && model.external_file
64812
ddbb89e7621d tuned signature;
wenzelm
parents: 64806
diff changeset
   189
            text <- read_file_content(file)
65160
6e042537555d incremental document changes;
wenzelm
parents: 65142
diff changeset
   190
            model1 <- model.change_text(text)
65116
06d9bcb66ef3 simplified;
wenzelm
parents: 65115
diff changeset
   191
          } yield (file, model1)).toList
06d9bcb66ef3 simplified;
wenzelm
parents: 65115
diff changeset
   192
        st.update_models(changed_models)
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   193
      })
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   194
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   195
66101
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   196
  /* overlays */
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 node_overlays(name: Document.Node.Name): Document.Node.Overlays =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   199
    state.value.overlays(name)
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
  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
   202
    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
   203
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   204
  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
   205
    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
   206
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66100
diff changeset
   207
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   208
  /* resolve dependencies */
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   209
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   210
  def resolve_dependencies(
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   211
    session: Session,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   212
    editor: Server.Editor,
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   213
    file_watcher: File_Watcher): (Boolean, Boolean) =
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   214
  {
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   215
    state.change_result(st =>
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   216
      {
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   217
        /* theory files */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   218
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   219
        val thys =
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   220
          (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
   221
           yield (model.node_name, Position.none)).toList
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   222
67292
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   223
        val thy_files1 = resources.dependencies(thys).theories
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   224
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   225
        val thy_files2 =
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   226
          (for {
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 67547
diff changeset
   227
            (_, model) <- st.models.iterator
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 67547
diff changeset
   228
            thy_name <- resources.make_theory_name(model.node_name)
67292
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   229
          } yield thy_name).toList
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   230
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   231
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   232
        /* auxiliary files */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   233
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   234
        val stable_tip_version =
64815
wenzelm
parents: 64812
diff changeset
   235
          if (st.models.forall(entry => entry._2.is_stable))
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   236
            session.current_state().stable_tip_version
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   237
          else None
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   238
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   239
        val aux_files =
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   240
          stable_tip_version match {
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   241
            case Some(version) => undefined_blobs(version.nodes)
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   242
            case None => Nil
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   243
          }
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   244
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   245
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   246
        /* loaded models */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   247
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   248
        val loaded_models =
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   249
          (for {
67292
386ddccfccbf implicit thy_load context for bibtex files (VSCode);
wenzelm
parents: 67104
diff changeset
   250
            node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   251
            file = node_file(node_name)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   252
            if !st.models.isDefinedAt(file)
64857
wenzelm
parents: 64856
diff changeset
   253
            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
   254
          }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   255
          yield {
66100
d1ad5a7458c2 proper treatment of editor overlays;
wenzelm
parents: 66086
diff changeset
   256
            val model = Document_Model.init(session, editor, node_name)
65160
6e042537555d incremental document changes;
wenzelm
parents: 65142
diff changeset
   257
            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
   258
            (file, model1)
65117
wenzelm
parents: 65116
diff changeset
   259
          }).toList
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   260
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   261
        val invoke_input = loaded_models.nonEmpty
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   262
        val invoke_load = stable_tip_version.isEmpty
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   263
65113
wenzelm
parents: 65112
diff changeset
   264
        ((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
   265
      })
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   266
  }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   267
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   268
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   269
  /* pending input */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   270
66676
39db5bb7eb0a recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents: 66674
diff changeset
   271
  def flush_input(session: Session, channel: Channel)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   272
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   273
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   274
      {
64719
wenzelm
parents: 64718
diff changeset
   275
        val changed_models =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   276
          (for {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   277
            file <- st.pending_input.iterator
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   278
            model <- st.models.get(file)
66676
39db5bb7eb0a recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents: 66674
diff changeset
   279
            (edits, model1) <-
39db5bb7eb0a recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents: 66674
diff changeset
   280
              model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   281
          } yield (edits, (file, model1))).toList
64707
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
   282
66676
39db5bb7eb0a recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents: 66674
diff changeset
   283
        for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
39db5bb7eb0a recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents: 66674
diff changeset
   284
          channel.write(Protocol.WorkspaceEdit(workspace_edits))
39db5bb7eb0a recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents: 66674
diff changeset
   285
39db5bb7eb0a recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents: 66674
diff changeset
   286
        session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
39db5bb7eb0a recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents: 66674
diff changeset
   287
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   288
        st.copy(
65112
wenzelm
parents: 65111
diff changeset
   289
          models = st.models ++ changed_models.iterator.map(_._2),
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   290
          pending_input = Set.empty)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   291
      })
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   292
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   293
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   294
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   295
  /* pending output */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   296
65118
31fd8e41be02 tuned signature;
wenzelm
parents: 65117
diff changeset
   297
  def update_output(changed_nodes: Traversable[JFile]): Unit =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   298
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   299
66138
f7ef4c50b747 added commands for spell-checker dictionary;
wenzelm
parents: 66101
diff changeset
   300
  def update_output_visible(): Unit =
f7ef4c50b747 added commands for spell-checker dictionary;
wenzelm
parents: 66101
diff changeset
   301
    state.change(st => st.copy(pending_output = st.pending_output ++
f7ef4c50b747 added commands for spell-checker dictionary;
wenzelm
parents: 66101
diff changeset
   302
      (for ((file, model) <- st.models.iterator if model.node_visible) yield file)))
f7ef4c50b747 added commands for spell-checker dictionary;
wenzelm
parents: 66101
diff changeset
   303
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   304
  def flush_output(channel: Channel): Boolean =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   305
  {
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   306
    state.change_result(st =>
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   307
      {
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   308
        val (postponed, flushed) =
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   309
          (for {
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   310
            file <- st.pending_output.iterator
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   311
            model <- st.models.get(file)
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   312
          } 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
   313
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   314
        val changed_iterator =
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   315
          for {
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   316
            (file, model, rendering) <- flushed.iterator
65115
93a0683e075a publish output more thoroughly;
wenzelm
parents: 65114
diff changeset
   317
            (changed_diags, changed_decos, model1) = model.publish(rendering)
93a0683e075a publish output more thoroughly;
wenzelm
parents: 65114
diff changeset
   318
            if changed_diags.isDefined || changed_decos.isDefined
65095
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   319
          }
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   320
          yield {
65115
93a0683e075a publish output more thoroughly;
wenzelm
parents: 65114
diff changeset
   321
            for (diags <- changed_diags)
93a0683e075a publish output more thoroughly;
wenzelm
parents: 65114
diff changeset
   322
              channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
65137
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   323
            if (pide_extensions) {
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   324
              for (decos <- changed_decos; deco <- decos)
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   325
                channel.write(rendering.decoration_output(deco).json(file))
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   326
            }
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   327
            (file, model1)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   328
          }
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   329
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   330
        (postponed.nonEmpty,
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   331
          st.copy(
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   332
            models = st.models ++ changed_iterator,
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65198
diff changeset
   333
            pending_output = postponed.map(_._1).toSet))
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   334
      }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   335
    )
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   336
  }
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   337
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   338
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   339
  /* output text */
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   340
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   341
  def output_text(s: String): String =
65137
812c35fbffa8 clarified options;
wenzelm
parents: 65132
diff changeset
   342
    if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   343
65107
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   344
  def output_xml(xml: XML.Tree): String =
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   345
    output_text(XML.content(xml))
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   346
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   347
  def output_pretty(body: XML.Body, margin: Int): String =
67547
aefe7a7b330a clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
wenzelm
parents: 67292
diff changeset
   348
    output_text(Pretty.string_of(body, margin = margin))
65107
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   349
  def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   350
  def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   351
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   352
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   353
  /* caret handling */
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   354
65191
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
   355
  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
   356
  { state.change(_.update_caret(caret)) }
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   357
66086
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
   358
  def get_caret(): Option[VSCode_Resources.Caret] =
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   359
  {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   360
    val st = state.value
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   361
    for {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   362
      (file, pos) <- st.caret
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   363
      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
   364
      offset <- model.content.doc.offset(pos)
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   365
    }
66086
3f7067ba5df3 clarified signature;
wenzelm
parents: 65976
diff changeset
   366
    yield VSCode_Resources.Caret(file, model, offset)
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   367
  }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   368
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65160
diff changeset
   369
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   370
  /* spell checker */
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   371
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   372
  val spell_checker = new Spell_Checker_Variable
368004bed323 decorations for spell-checker;
wenzelm
parents: 65137
diff changeset
   373
  spell_checker.update(options)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   374
}