src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Mon Sep 18 18:19:06 2017 +0200 (22 months ago)
changeset 66676 39db5bb7eb0a
parent 66674 30d5195299e2
child 66714 9fc4e144693c
permissions -rw-r--r--
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm@64623
     1
/*  Title:      Tools/VSCode/src/vscode_resources.scala
wenzelm@64605
     2
    Author:     Makarius
wenzelm@64605
     3
wenzelm@64729
     4
Resources for VSCode Language Server: file-system access and global state.
wenzelm@64605
     5
*/
wenzelm@64605
     6
wenzelm@64605
     7
package isabelle.vscode
wenzelm@64605
     8
wenzelm@64605
     9
wenzelm@64605
    10
import isabelle._
wenzelm@64605
    11
wenzelm@64605
    12
import java.io.{File => JFile}
wenzelm@64605
    13
wenzelm@64824
    14
import scala.util.parsing.input.Reader
wenzelm@64727
    15
wenzelm@64605
    16
wenzelm@64623
    17
object VSCode_Resources
wenzelm@64605
    18
{
wenzelm@64703
    19
  /* internal state */
wenzelm@64703
    20
wenzelm@64703
    21
  sealed case class State(
wenzelm@64777
    22
    models: Map[JFile, Document_Model] = Map.empty,
wenzelm@65926
    23
    caret: Option[(JFile, Line.Position)] = None,
wenzelm@66101
    24
    overlays: Document.Overlays = Document.Overlays.empty,
wenzelm@64777
    25
    pending_input: Set[JFile] = Set.empty,
wenzelm@65926
    26
    pending_output: Set[JFile] = Set.empty)
wenzelm@64800
    27
  {
wenzelm@65113
    28
    def update_models(changed: Traversable[(JFile, Document_Model)]): State =
wenzelm@65111
    29
      copy(
wenzelm@65113
    30
        models = models ++ changed,
wenzelm@65113
    31
        pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
wenzelm@65113
    32
        pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file })
wenzelm@65111
    33
wenzelm@65926
    34
    def update_caret(new_caret: Option[(JFile, Line.Position)]): State =
wenzelm@65926
    35
      if (caret == new_caret) this
wenzelm@65926
    36
      else
wenzelm@65926
    37
        copy(
wenzelm@65926
    38
          caret = new_caret,
wenzelm@65926
    39
          pending_input = pending_input ++ caret.map(_._1) ++ new_caret.map(_._1))
wenzelm@65926
    40
wenzelm@65926
    41
    def get_caret(file: JFile): Option[Line.Position] =
wenzelm@65926
    42
      caret match {
wenzelm@65926
    43
        case Some((caret_file, caret_pos)) if caret_file == file => Some(caret_pos)
wenzelm@65926
    44
        case _ => None
wenzelm@65926
    45
      }
wenzelm@65926
    46
wenzelm@64800
    47
    lazy val document_blobs: Document.Blobs =
wenzelm@64800
    48
      Document.Blobs(
wenzelm@64800
    49
        (for {
wenzelm@64800
    50
          (_, model) <- models.iterator
wenzelm@64800
    51
          blob <- model.get_blob
wenzelm@64800
    52
        } yield (model.node_name -> blob)).toMap)
wenzelm@66101
    53
wenzelm@66101
    54
    def change_overlay(insert: Boolean, file: JFile,
wenzelm@66101
    55
        command: Command, fn: String, args: List[String]): State =
wenzelm@66101
    56
      copy(
wenzelm@66101
    57
        overlays =
wenzelm@66101
    58
          if (insert) overlays.insert(command, fn, args)
wenzelm@66101
    59
          else overlays.remove(command, fn, args),
wenzelm@66101
    60
        pending_input = pending_input + file)
wenzelm@64800
    61
  }
wenzelm@66086
    62
wenzelm@66086
    63
wenzelm@66086
    64
  /* caret */
wenzelm@66086
    65
wenzelm@66086
    66
  sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset)
wenzelm@66086
    67
  {
wenzelm@66086
    68
    def node_name: Document.Node.Name = model.node_name
wenzelm@66086
    69
  }
wenzelm@64605
    70
}
wenzelm@64605
    71
wenzelm@64623
    72
class VSCode_Resources(
wenzelm@65361
    73
    val options: Options,
wenzelm@65361
    74
    session_base: Sessions.Base,
wenzelm@65361
    75
    log: Logger = No_Logger)
wenzelm@65441
    76
  extends Resources(session_base, log = log)
wenzelm@64605
    77
{
wenzelm@64703
    78
  private val state = Synchronized(VSCode_Resources.State())
wenzelm@64703
    79
wenzelm@64703
    80
wenzelm@65137
    81
  /* options */
wenzelm@65137
    82
wenzelm@65137
    83
  def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
wenzelm@65137
    84
  def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
wenzelm@65137
    85
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
wenzelm@65137
    86
  def message_margin: Int = options.int("vscode_message_margin")
wenzelm@65137
    87
wenzelm@65137
    88
wenzelm@64703
    89
  /* document node name */
wenzelm@64703
    90
wenzelm@64777
    91
  def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
wenzelm@64777
    92
wenzelm@64777
    93
  def node_name(file: JFile): Document.Node.Name =
wenzelm@66195
    94
    session_base.known.get_file(file, bootstrap = true) getOrElse {
wenzelm@65501
    95
      val node = file.getPath
wenzelm@65532
    96
      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
wenzelm@65501
    97
        case (true, theory) => Document.Node.Name.loaded_theory(theory)
wenzelm@65501
    98
        case (false, theory) =>
wenzelm@65501
    99
          val master_dir = if (theory == "") "" else file.getParent
wenzelm@65501
   100
          Document.Node.Name(node, master_dir, theory)
wenzelm@65501
   101
      }
wenzelm@65472
   102
    }
wenzelm@64703
   103
wenzelm@64759
   104
  override def append(dir: String, source_path: Path): String =
wenzelm@64716
   105
  {
wenzelm@64759
   106
    val path = source_path.expand
wenzelm@64777
   107
    if (dir == "" || path.is_absolute) File.platform_path(path)
wenzelm@64759
   108
    else if (path.is_current) dir
wenzelm@64777
   109
    else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
wenzelm@64777
   110
      dir + JFile.separator + File.platform_path(path)
wenzelm@64777
   111
    else if (path.is_basic) dir + File.platform_path(path)
wenzelm@66235
   112
    else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
wenzelm@64716
   113
  }
wenzelm@64716
   114
wenzelm@66152
   115
  def get_models: Map[JFile, Document_Model] = state.value.models
wenzelm@66152
   116
  def get_model(file: JFile): Option[Document_Model] = get_models.get(file)
wenzelm@64834
   117
  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
wenzelm@64834
   118
wenzelm@64834
   119
wenzelm@64834
   120
  /* file content */
wenzelm@64834
   121
wenzelm@64834
   122
  def read_file_content(file: JFile): Option[String] =
wenzelm@64834
   123
    try { Some(Line.normalize(File.read(file))) }
wenzelm@64834
   124
    catch { case ERROR(_) => None }
wenzelm@64834
   125
wenzelm@64834
   126
  def get_file_content(file: JFile): Option[String] =
wenzelm@64834
   127
    get_model(file) match {
wenzelm@64834
   128
      case Some(model) => Some(model.content.text)
wenzelm@64834
   129
      case None => read_file_content(file)
wenzelm@64834
   130
    }
wenzelm@64834
   131
wenzelm@64727
   132
  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
wenzelm@64727
   133
  {
wenzelm@64777
   134
    val file = node_file(name)
wenzelm@64777
   135
    get_model(file) match {
wenzelm@64830
   136
      case Some(model) => f(Scan.char_reader(model.content.text))
wenzelm@64777
   137
      case None if file.isFile =>
wenzelm@64727
   138
        val reader = Scan.byte_reader(file)
wenzelm@64727
   139
        try { f(reader) } finally { reader.close }
wenzelm@64777
   140
      case None =>
wenzelm@64777
   141
        error("No such file: " + quote(file.toString))
wenzelm@64727
   142
    }
wenzelm@64727
   143
  }
wenzelm@64727
   144
wenzelm@64703
   145
wenzelm@64703
   146
  /* document models */
wenzelm@64703
   147
wenzelm@64800
   148
  def visible_node(name: Document.Node.Name): Boolean =
wenzelm@64800
   149
    get_model(name) match {
wenzelm@64800
   150
      case Some(model) => model.node_visible
wenzelm@64800
   151
      case None => false
wenzelm@64800
   152
    }
wenzelm@64800
   153
wenzelm@66100
   154
  def change_model(
wenzelm@66100
   155
    session: Session,
wenzelm@66100
   156
    editor: Server.Editor,
wenzelm@66100
   157
    file: JFile,
wenzelm@66674
   158
    version: Long,
wenzelm@66100
   159
    text: String,
wenzelm@66100
   160
    range: Option[Line.Range] = None)
wenzelm@64703
   161
  {
wenzelm@64703
   162
    state.change(st =>
wenzelm@64709
   163
      {
wenzelm@66100
   164
        val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
wenzelm@66674
   165
        val model1 =
wenzelm@66674
   166
          (model.change_text(text, range) getOrElse model).set_version(version).external(false)
wenzelm@65114
   167
        st.update_models(Some(file -> model1))
wenzelm@64709
   168
      })
wenzelm@64703
   169
  }
wenzelm@64703
   170
wenzelm@65111
   171
  def close_model(file: JFile): Boolean =
wenzelm@64710
   172
    state.change_result(st =>
wenzelm@64777
   173
      st.models.get(file) match {
wenzelm@65111
   174
        case None => (false, st)
wenzelm@65113
   175
        case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
wenzelm@64710
   176
      })
wenzelm@64710
   177
wenzelm@65116
   178
  def sync_models(changed_files: Set[JFile]): Unit =
wenzelm@65116
   179
    state.change(st =>
wenzelm@64710
   180
      {
wenzelm@64719
   181
        val changed_models =
wenzelm@64710
   182
          (for {
wenzelm@64777
   183
            (file, model) <- st.models.iterator
wenzelm@64777
   184
            if changed_files(file) && model.external_file
wenzelm@64812
   185
            text <- read_file_content(file)
wenzelm@65160
   186
            model1 <- model.change_text(text)
wenzelm@65116
   187
          } yield (file, model1)).toList
wenzelm@65116
   188
        st.update_models(changed_models)
wenzelm@64710
   189
      })
wenzelm@64710
   190
wenzelm@64703
   191
wenzelm@66101
   192
  /* overlays */
wenzelm@66101
   193
wenzelm@66101
   194
  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
wenzelm@66101
   195
    state.value.overlays(name)
wenzelm@66101
   196
wenzelm@66101
   197
  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@66101
   198
    state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args))
wenzelm@66101
   199
wenzelm@66101
   200
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@66101
   201
    state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args))
wenzelm@66101
   202
wenzelm@66101
   203
wenzelm@64727
   204
  /* resolve dependencies */
wenzelm@64727
   205
wenzelm@66100
   206
  def resolve_dependencies(
wenzelm@66100
   207
    session: Session,
wenzelm@66100
   208
    editor: Server.Editor,
wenzelm@66100
   209
    file_watcher: File_Watcher): (Boolean, Boolean) =
wenzelm@64727
   210
  {
wenzelm@64727
   211
    state.change_result(st =>
wenzelm@64727
   212
      {
wenzelm@64800
   213
        /* theory files */
wenzelm@64800
   214
wenzelm@64731
   215
        val thys =
wenzelm@64731
   216
          (for ((_, model) <- st.models.iterator if model.is_theory)
wenzelm@64731
   217
           yield (model.node_name, Position.none)).toList
wenzelm@64731
   218
wenzelm@65359
   219
        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
wenzelm@64800
   220
wenzelm@64800
   221
wenzelm@64800
   222
        /* auxiliary files */
wenzelm@64800
   223
wenzelm@64800
   224
        val stable_tip_version =
wenzelm@64815
   225
          if (st.models.forall(entry => entry._2.is_stable))
wenzelm@64800
   226
            session.current_state().stable_tip_version
wenzelm@64800
   227
          else None
wenzelm@64800
   228
wenzelm@64800
   229
        val aux_files =
wenzelm@64800
   230
          stable_tip_version match {
wenzelm@64800
   231
            case Some(version) => undefined_blobs(version.nodes)
wenzelm@64800
   232
            case None => Nil
wenzelm@64800
   233
          }
wenzelm@64800
   234
wenzelm@64800
   235
wenzelm@64800
   236
        /* loaded models */
wenzelm@64800
   237
wenzelm@64727
   238
        val loaded_models =
wenzelm@64731
   239
          (for {
wenzelm@64800
   240
            node_name <- thy_files.iterator ++ aux_files.iterator
wenzelm@64800
   241
            file = node_file(node_name)
wenzelm@64777
   242
            if !st.models.isDefinedAt(file)
wenzelm@64857
   243
            text <- { file_watcher.register_parent(file); read_file_content(file) }
wenzelm@64727
   244
          }
wenzelm@64727
   245
          yield {
wenzelm@66100
   246
            val model = Document_Model.init(session, editor, node_name)
wenzelm@65160
   247
            val model1 = (model.change_text(text) getOrElse model).external(true)
wenzelm@64777
   248
            (file, model1)
wenzelm@65117
   249
          }).toList
wenzelm@64731
   250
wenzelm@64800
   251
        val invoke_input = loaded_models.nonEmpty
wenzelm@64800
   252
        val invoke_load = stable_tip_version.isEmpty
wenzelm@64800
   253
wenzelm@65113
   254
        ((invoke_input, invoke_load), st.update_models(loaded_models))
wenzelm@64727
   255
      })
wenzelm@64727
   256
  }
wenzelm@64727
   257
wenzelm@64727
   258
wenzelm@64703
   259
  /* pending input */
wenzelm@64703
   260
wenzelm@66676
   261
  def flush_input(session: Session, channel: Channel)
wenzelm@64703
   262
  {
wenzelm@64703
   263
    state.change(st =>
wenzelm@64703
   264
      {
wenzelm@64719
   265
        val changed_models =
wenzelm@64703
   266
          (for {
wenzelm@64777
   267
            file <- st.pending_input.iterator
wenzelm@64777
   268
            model <- st.models.get(file)
wenzelm@66676
   269
            (edits, model1) <-
wenzelm@66676
   270
              model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
wenzelm@64777
   271
          } yield (edits, (file, model1))).toList
wenzelm@64707
   272
wenzelm@66676
   273
        for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
wenzelm@66676
   274
          channel.write(Protocol.WorkspaceEdit(workspace_edits))
wenzelm@66676
   275
wenzelm@66676
   276
        session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
wenzelm@66676
   277
wenzelm@64703
   278
        st.copy(
wenzelm@65112
   279
          models = st.models ++ changed_models.iterator.map(_._2),
wenzelm@64703
   280
          pending_input = Set.empty)
wenzelm@64703
   281
      })
wenzelm@64703
   282
  }
wenzelm@64703
   283
wenzelm@64703
   284
wenzelm@64703
   285
  /* pending output */
wenzelm@64703
   286
wenzelm@65118
   287
  def update_output(changed_nodes: Traversable[JFile]): Unit =
wenzelm@64703
   288
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
wenzelm@64703
   289
wenzelm@66138
   290
  def update_output_visible(): Unit =
wenzelm@66138
   291
    state.change(st => st.copy(pending_output = st.pending_output ++
wenzelm@66138
   292
      (for ((file, model) <- st.models.iterator if model.node_visible) yield file)))
wenzelm@66138
   293
wenzelm@65232
   294
  def flush_output(channel: Channel): Boolean =
wenzelm@64703
   295
  {
wenzelm@65232
   296
    state.change_result(st =>
wenzelm@64703
   297
      {
wenzelm@65232
   298
        val (postponed, flushed) =
wenzelm@65232
   299
          (for {
wenzelm@65232
   300
            file <- st.pending_output.iterator
wenzelm@65232
   301
            model <- st.models.get(file)
wenzelm@65232
   302
          } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
wenzelm@65232
   303
wenzelm@64703
   304
        val changed_iterator =
wenzelm@64703
   305
          for {
wenzelm@65232
   306
            (file, model, rendering) <- flushed.iterator
wenzelm@65115
   307
            (changed_diags, changed_decos, model1) = model.publish(rendering)
wenzelm@65115
   308
            if changed_diags.isDefined || changed_decos.isDefined
wenzelm@65095
   309
          }
wenzelm@65095
   310
          yield {
wenzelm@65115
   311
            for (diags <- changed_diags)
wenzelm@65115
   312
              channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
wenzelm@65137
   313
            if (pide_extensions) {
wenzelm@65137
   314
              for (decos <- changed_decos; deco <- decos)
wenzelm@65137
   315
                channel.write(rendering.decoration_output(deco).json(file))
wenzelm@65137
   316
            }
wenzelm@64777
   317
            (file, model1)
wenzelm@64703
   318
          }
wenzelm@65232
   319
wenzelm@65232
   320
        (postponed.nonEmpty,
wenzelm@65232
   321
          st.copy(
wenzelm@65232
   322
            models = st.models ++ changed_iterator,
wenzelm@65232
   323
            pending_output = postponed.map(_._1).toSet))
wenzelm@64703
   324
      }
wenzelm@64703
   325
    )
wenzelm@64703
   326
  }
wenzelm@64870
   327
wenzelm@64870
   328
wenzelm@64870
   329
  /* output text */
wenzelm@64870
   330
wenzelm@64870
   331
  def output_text(s: String): String =
wenzelm@65137
   332
    if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
wenzelm@64870
   333
wenzelm@65107
   334
  def output_xml(xml: XML.Tree): String =
wenzelm@65107
   335
    output_text(XML.content(xml))
wenzelm@65107
   336
wenzelm@64870
   337
  def output_pretty(body: XML.Body, margin: Int): String =
wenzelm@64870
   338
    output_text(Pretty.string_of(body, margin))
wenzelm@65107
   339
  def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
wenzelm@65107
   340
  def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
wenzelm@65142
   341
wenzelm@65142
   342
wenzelm@65189
   343
  /* caret handling */
wenzelm@65189
   344
wenzelm@65191
   345
  def update_caret(caret: Option[(JFile, Line.Position)])
wenzelm@65926
   346
  { state.change(_.update_caret(caret)) }
wenzelm@65189
   347
wenzelm@66086
   348
  def get_caret(): Option[VSCode_Resources.Caret] =
wenzelm@65189
   349
  {
wenzelm@65189
   350
    val st = state.value
wenzelm@65189
   351
    for {
wenzelm@65189
   352
      (file, pos) <- st.caret
wenzelm@65189
   353
      model <- st.models.get(file)
wenzelm@65191
   354
      offset <- model.content.doc.offset(pos)
wenzelm@65189
   355
    }
wenzelm@66086
   356
    yield VSCode_Resources.Caret(file, model, offset)
wenzelm@65189
   357
  }
wenzelm@65189
   358
wenzelm@65189
   359
wenzelm@65142
   360
  /* spell checker */
wenzelm@65142
   361
wenzelm@65142
   362
  val spell_checker = new Spell_Checker_Variable
wenzelm@65142
   363
  spell_checker.update(options)
wenzelm@64605
   364
}