src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Sun, 05 Mar 2017 14:11:24 +0100
changeset 65113 6058e7d31fe6
parent 65112 b3904f683ef5
child 65114 200b787ceb51
permissions -rw-r--r--
tuned;
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,
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    23
    pending_input: Set[JFile] = Set.empty,
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    24
    pending_output: Set[JFile] = Set.empty)
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    25
  {
65113
wenzelm
parents: 65112
diff changeset
    26
    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
    27
      copy(
65113
wenzelm
parents: 65112
diff changeset
    28
        models = models ++ changed,
wenzelm
parents: 65112
diff changeset
    29
        pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
wenzelm
parents: 65112
diff changeset
    30
        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
    31
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    32
    lazy val document_blobs: Document.Blobs =
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    33
      Document.Blobs(
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    34
        (for {
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    35
          (_, model) <- models.iterator
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    36
          blob <- model.get_blob
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    37
        } yield (model.node_name -> blob)).toMap)
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
    38
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    39
}
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    40
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64605
diff changeset
    41
class VSCode_Resources(
64854
f5aa712e6250 tuned signature;
wenzelm
parents: 64839
diff changeset
    42
  val options: Options,
f5aa712e6250 tuned signature;
wenzelm
parents: 64839
diff changeset
    43
  val text_length: Text.Length,
64856
5e9bf964510a clarified modules;
wenzelm
parents: 64854
diff changeset
    44
  base: Sessions.Base,
64854
f5aa712e6250 tuned signature;
wenzelm
parents: 64839
diff changeset
    45
  log: Logger = No_Logger) extends Resources(base, log)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    46
{
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    47
  private val state = Synchronized(VSCode_Resources.State())
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    48
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    49
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    50
  /* document node name */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    51
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    52
  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
    53
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    54
  def node_name(file: JFile): Document.Node.Name =
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    55
  {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    56
    val node = file.getPath
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    57
    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    58
    val master_dir = if (theory == "") "" else file.getParent
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    59
    Document.Node.Name(node, master_dir, theory)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    60
  }
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    61
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
    62
  override def append(dir: String, source_path: Path): String =
64716
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    63
  {
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
    64
    val path = source_path.expand
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    65
    if (dir == "" || path.is_absolute) File.platform_path(path)
64759
100941134718 clarified master_dir: file-URL;
wenzelm
parents: 64754
diff changeset
    66
    else if (path.is_current) dir
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    67
    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
    68
      dir + JFile.separator + File.platform_path(path)
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    69
    else if (path.is_basic) dir + File.platform_path(path)
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    70
    else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
64716
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    71
  }
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    72
64834
wenzelm
parents: 64833
diff changeset
    73
  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
wenzelm
parents: 64833
diff changeset
    74
  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
wenzelm
parents: 64833
diff changeset
    75
wenzelm
parents: 64833
diff changeset
    76
wenzelm
parents: 64833
diff changeset
    77
  /* file content */
wenzelm
parents: 64833
diff changeset
    78
wenzelm
parents: 64833
diff changeset
    79
  def read_file_content(file: JFile): Option[String] =
wenzelm
parents: 64833
diff changeset
    80
    try { Some(Line.normalize(File.read(file))) }
wenzelm
parents: 64833
diff changeset
    81
    catch { case ERROR(_) => None }
wenzelm
parents: 64833
diff changeset
    82
wenzelm
parents: 64833
diff changeset
    83
  def get_file_content(file: JFile): Option[String] =
wenzelm
parents: 64833
diff changeset
    84
    get_model(file) match {
wenzelm
parents: 64833
diff changeset
    85
      case Some(model) => Some(model.content.text)
wenzelm
parents: 64833
diff changeset
    86
      case None => read_file_content(file)
wenzelm
parents: 64833
diff changeset
    87
    }
wenzelm
parents: 64833
diff changeset
    88
wenzelm
parents: 64833
diff changeset
    89
  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
wenzelm
parents: 64833
diff changeset
    90
    for {
wenzelm
parents: 64833
diff changeset
    91
      (_, model) <- state.value.models.iterator
wenzelm
parents: 64833
diff changeset
    92
      Text.Info(range, entry) <- model.content.bibtex_entries.iterator
wenzelm
parents: 64833
diff changeset
    93
    } yield Text.Info(range, (entry, model))
wenzelm
parents: 64833
diff changeset
    94
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
    95
  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
    96
  {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    97
    val file = node_file(name)
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
    98
    get_model(file) match {
64830
9bc44bef99e6 more explocit Document_Model.Content;
wenzelm
parents: 64824
diff changeset
    99
      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
   100
      case None if file.isFile =>
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   101
        val reader = Scan.byte_reader(file)
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   102
        try { f(reader) } finally { reader.close }
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   103
      case None =>
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   104
        error("No such file: " + quote(file.toString))
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   105
    }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   106
  }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   107
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   108
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   109
  /* document models */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   110
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   111
  def visible_node(name: Document.Node.Name): Boolean =
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   112
    get_model(name) match {
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   113
      case Some(model) => model.node_visible
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   114
      case None => false
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   115
    }
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   116
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   117
  def update_model(session: Session, file: JFile, text: String)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   118
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   119
    state.change(st =>
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
   120
      {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   121
        val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   122
        val model1 = (model.update_text(text) getOrElse model).external(false)
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
   123
        st.copy(
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   124
          models = st.models + (file -> model1),
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   125
          pending_input = st.pending_input + file,
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   126
          pending_output = st.pending_output ++
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   127
            (if (model.node_visible == model1.node_visible) None else Some(file)))
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
   128
      })
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   129
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   130
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   131
  def close_model(file: JFile): Boolean =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   132
    state.change_result(st =>
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   133
      st.models.get(file) match {
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   134
        case None => (false, st)
65113
wenzelm
parents: 65112
diff changeset
   135
        case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   136
      })
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   137
64722
6df73de0d3c7 tuned signature;
wenzelm
parents: 64721
diff changeset
   138
  def sync_models(changed_files: Set[JFile]): Boolean =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   139
    state.change_result(st =>
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   140
      {
64719
wenzelm
parents: 64718
diff changeset
   141
        val changed_models =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   142
          (for {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   143
            (file, model) <- st.models.iterator
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   144
            if changed_files(file) && model.external_file
64812
ddbb89e7621d tuned signature;
wenzelm
parents: 64806
diff changeset
   145
            text <- read_file_content(file)
64779
wenzelm
parents: 64777
diff changeset
   146
            model1 <- model.update_text(text)
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   147
          } yield (file, model1)).toMap
64719
wenzelm
parents: 64718
diff changeset
   148
        if (changed_models.isEmpty) (false, st)
65113
wenzelm
parents: 65112
diff changeset
   149
        else (true, st.update_models(changed_models))
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   150
      })
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   151
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   152
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   153
  /* resolve dependencies */
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   154
64857
wenzelm
parents: 64856
diff changeset
   155
  def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) =
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   156
  {
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   157
    state.change_result(st =>
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   158
      {
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   159
        /* theory files */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   160
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   161
        val thys =
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   162
          (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
   163
           yield (model.node_name, Position.none)).toList
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   164
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   165
        val thy_files = thy_info.dependencies("", thys).deps.map(_.name)
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   166
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   167
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   168
        /* auxiliary files */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   169
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   170
        val stable_tip_version =
64815
wenzelm
parents: 64812
diff changeset
   171
          if (st.models.forall(entry => entry._2.is_stable))
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   172
            session.current_state().stable_tip_version
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   173
          else None
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   174
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   175
        val aux_files =
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   176
          stable_tip_version match {
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   177
            case Some(version) => undefined_blobs(version.nodes)
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   178
            case None => Nil
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   179
          }
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   180
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   181
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   182
        /* loaded models */
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   183
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   184
        val loaded_models =
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   185
          (for {
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   186
            node_name <- thy_files.iterator ++ aux_files.iterator
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   187
            file = node_file(node_name)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   188
            if !st.models.isDefinedAt(file)
64857
wenzelm
parents: 64856
diff changeset
   189
            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
   190
          }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   191
          yield {
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   192
            val model = Document_Model.init(session, node_name)
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   193
            val model1 = (model.update_text(text) getOrElse model).external(true)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   194
            (file, model1)
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   195
          }).toMap
64731
84192ecae582 just one synchronized access to global state: works recursively on JVM;
wenzelm
parents: 64729
diff changeset
   196
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   197
        val invoke_input = loaded_models.nonEmpty
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   198
        val invoke_load = stable_tip_version.isEmpty
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   199
65113
wenzelm
parents: 65112
diff changeset
   200
        ((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
   201
      })
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   202
  }
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   203
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64726
diff changeset
   204
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   205
  /* pending input */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   206
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   207
  def flush_input(session: Session)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   208
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   209
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   210
      {
64719
wenzelm
parents: 64718
diff changeset
   211
        val changed_models =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   212
          (for {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   213
            file <- st.pending_input.iterator
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   214
            model <- st.models.get(file)
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   215
            (edits, model1) <- model.flush_edits(st.document_blobs)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   216
          } yield (edits, (file, model1))).toList
64707
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
   217
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64796
diff changeset
   218
        session.update(st.document_blobs, changed_models.flatMap(_._1))
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   219
        st.copy(
65112
wenzelm
parents: 65111
diff changeset
   220
          models = st.models ++ changed_models.iterator.map(_._2),
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   221
          pending_input = Set.empty)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   222
      })
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   223
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   224
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   225
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   226
  /* pending output */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   227
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   228
  def update_output(changed_nodes: List[JFile]): Unit =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   229
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   230
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   231
  def flush_output(channel: Channel)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   232
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   233
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   234
      {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   235
        val changed_iterator =
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   236
          for {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   237
            file <- st.pending_output.iterator
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   238
            model <- st.models.get(file)
64704
08c2d80428ff re-use options from resources;
wenzelm
parents: 64703
diff changeset
   239
            rendering = model.rendering()
65095
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   240
            ((diagnostics, decorations), model1) <- model.publish(rendering)
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   241
          }
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   242
          yield {
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   243
            if (diagnostics.nonEmpty)
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   244
              channel.write(
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   245
                Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diagnostics)))
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   246
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   247
            for (decoration <- decorations)
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   248
              channel.write(rendering.decoration_output(decoration).json(file))
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 64877
diff changeset
   249
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64775
diff changeset
   250
            (file, model1)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   251
          }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   252
        st.copy(
65112
wenzelm
parents: 65111
diff changeset
   253
          models = st.models ++ changed_iterator,
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   254
          pending_output = Set.empty)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   255
      }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   256
    )
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   257
  }
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   258
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   259
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   260
  /* output text */
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   261
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   262
  def decode_text: Boolean = options.bool("vscode_unicode_symbols")
65107
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   263
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   264
  def message_margin: Int = options.int("vscode_message_margin")
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   265
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   266
  def output_text(s: String): String =
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   267
    if (decode_text) Symbol.decode(s) else Symbol.encode(s)
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   268
65107
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   269
  def output_xml(xml: XML.Tree): String =
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   270
    output_text(XML.content(xml))
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   271
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   272
  def output_pretty(body: XML.Body, margin: Int): String =
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   273
    output_text(Pretty.string_of(body, margin))
65107
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   274
  def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65095
diff changeset
   275
  def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   276
}