src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Mon Jun 26 15:57:20 2017 +0200 (2017-06-26 ago)
changeset 66195 bb886f13623a
parent 66152 18e1aba549f6
child 66234 836898197296
permissions -rw-r--r--
proper bootstrap_name (amending b42743f5b595);
wenzelm@64624
     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@64624
    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@64624
    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@64777
   112
    else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
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@66100
   158
    text: String,
wenzelm@66100
   159
    range: Option[Line.Range] = None)
wenzelm@64703
   160
  {
wenzelm@64703
   161
    state.change(st =>
wenzelm@64709
   162
      {
wenzelm@66100
   163
        val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
wenzelm@65160
   164
        val model1 = (model.change_text(text, range) getOrElse model).external(false)
wenzelm@65114
   165
        st.update_models(Some(file -> model1))
wenzelm@64709
   166
      })
wenzelm@64703
   167
  }
wenzelm@64703
   168
wenzelm@65111
   169
  def close_model(file: JFile): Boolean =
wenzelm@64710
   170
    state.change_result(st =>
wenzelm@64777
   171
      st.models.get(file) match {
wenzelm@65111
   172
        case None => (false, st)
wenzelm@65113
   173
        case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
wenzelm@64710
   174
      })
wenzelm@64710
   175
wenzelm@65116
   176
  def sync_models(changed_files: Set[JFile]): Unit =
wenzelm@65116
   177
    state.change(st =>
wenzelm@64710
   178
      {
wenzelm@64719
   179
        val changed_models =
wenzelm@64710
   180
          (for {
wenzelm@64777
   181
            (file, model) <- st.models.iterator
wenzelm@64777
   182
            if changed_files(file) && model.external_file
wenzelm@64812
   183
            text <- read_file_content(file)
wenzelm@65160
   184
            model1 <- model.change_text(text)
wenzelm@65116
   185
          } yield (file, model1)).toList
wenzelm@65116
   186
        st.update_models(changed_models)
wenzelm@64710
   187
      })
wenzelm@64710
   188
wenzelm@64703
   189
wenzelm@66101
   190
  /* overlays */
wenzelm@66101
   191
wenzelm@66101
   192
  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
wenzelm@66101
   193
    state.value.overlays(name)
wenzelm@66101
   194
wenzelm@66101
   195
  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@66101
   196
    state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args))
wenzelm@66101
   197
wenzelm@66101
   198
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@66101
   199
    state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args))
wenzelm@66101
   200
wenzelm@66101
   201
wenzelm@64727
   202
  /* resolve dependencies */
wenzelm@64727
   203
wenzelm@66100
   204
  def resolve_dependencies(
wenzelm@66100
   205
    session: Session,
wenzelm@66100
   206
    editor: Server.Editor,
wenzelm@66100
   207
    file_watcher: File_Watcher): (Boolean, Boolean) =
wenzelm@64727
   208
  {
wenzelm@64727
   209
    state.change_result(st =>
wenzelm@64727
   210
      {
wenzelm@64800
   211
        /* theory files */
wenzelm@64800
   212
wenzelm@64731
   213
        val thys =
wenzelm@64731
   214
          (for ((_, model) <- st.models.iterator if model.is_theory)
wenzelm@64731
   215
           yield (model.node_name, Position.none)).toList
wenzelm@64731
   216
wenzelm@65359
   217
        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
wenzelm@64800
   218
wenzelm@64800
   219
wenzelm@64800
   220
        /* auxiliary files */
wenzelm@64800
   221
wenzelm@64800
   222
        val stable_tip_version =
wenzelm@64815
   223
          if (st.models.forall(entry => entry._2.is_stable))
wenzelm@64800
   224
            session.current_state().stable_tip_version
wenzelm@64800
   225
          else None
wenzelm@64800
   226
wenzelm@64800
   227
        val aux_files =
wenzelm@64800
   228
          stable_tip_version match {
wenzelm@64800
   229
            case Some(version) => undefined_blobs(version.nodes)
wenzelm@64800
   230
            case None => Nil
wenzelm@64800
   231
          }
wenzelm@64800
   232
wenzelm@64800
   233
wenzelm@64800
   234
        /* loaded models */
wenzelm@64800
   235
wenzelm@64727
   236
        val loaded_models =
wenzelm@64731
   237
          (for {
wenzelm@64800
   238
            node_name <- thy_files.iterator ++ aux_files.iterator
wenzelm@64800
   239
            file = node_file(node_name)
wenzelm@64777
   240
            if !st.models.isDefinedAt(file)
wenzelm@64857
   241
            text <- { file_watcher.register_parent(file); read_file_content(file) }
wenzelm@64727
   242
          }
wenzelm@64727
   243
          yield {
wenzelm@66100
   244
            val model = Document_Model.init(session, editor, node_name)
wenzelm@65160
   245
            val model1 = (model.change_text(text) getOrElse model).external(true)
wenzelm@64777
   246
            (file, model1)
wenzelm@65117
   247
          }).toList
wenzelm@64731
   248
wenzelm@64800
   249
        val invoke_input = loaded_models.nonEmpty
wenzelm@64800
   250
        val invoke_load = stable_tip_version.isEmpty
wenzelm@64800
   251
wenzelm@65113
   252
        ((invoke_input, invoke_load), st.update_models(loaded_models))
wenzelm@64727
   253
      })
wenzelm@64727
   254
  }
wenzelm@64727
   255
wenzelm@64727
   256
wenzelm@64703
   257
  /* pending input */
wenzelm@64703
   258
wenzelm@64703
   259
  def flush_input(session: Session)
wenzelm@64703
   260
  {
wenzelm@64703
   261
    state.change(st =>
wenzelm@64703
   262
      {
wenzelm@64719
   263
        val changed_models =
wenzelm@64703
   264
          (for {
wenzelm@64777
   265
            file <- st.pending_input.iterator
wenzelm@64777
   266
            model <- st.models.get(file)
wenzelm@65926
   267
            (edits, model1) <- model.flush_edits(st.document_blobs, st.get_caret(file))
wenzelm@64777
   268
          } yield (edits, (file, model1))).toList
wenzelm@64707
   269
wenzelm@64800
   270
        session.update(st.document_blobs, changed_models.flatMap(_._1))
wenzelm@64703
   271
        st.copy(
wenzelm@65112
   272
          models = st.models ++ changed_models.iterator.map(_._2),
wenzelm@64703
   273
          pending_input = Set.empty)
wenzelm@64703
   274
      })
wenzelm@64703
   275
  }
wenzelm@64703
   276
wenzelm@64703
   277
wenzelm@64703
   278
  /* pending output */
wenzelm@64703
   279
wenzelm@65118
   280
  def update_output(changed_nodes: Traversable[JFile]): Unit =
wenzelm@64703
   281
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
wenzelm@64703
   282
wenzelm@66138
   283
  def update_output_visible(): Unit =
wenzelm@66138
   284
    state.change(st => st.copy(pending_output = st.pending_output ++
wenzelm@66138
   285
      (for ((file, model) <- st.models.iterator if model.node_visible) yield file)))
wenzelm@66138
   286
wenzelm@65232
   287
  def flush_output(channel: Channel): Boolean =
wenzelm@64703
   288
  {
wenzelm@65232
   289
    state.change_result(st =>
wenzelm@64703
   290
      {
wenzelm@65232
   291
        val (postponed, flushed) =
wenzelm@65232
   292
          (for {
wenzelm@65232
   293
            file <- st.pending_output.iterator
wenzelm@65232
   294
            model <- st.models.get(file)
wenzelm@65232
   295
          } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
wenzelm@65232
   296
wenzelm@64703
   297
        val changed_iterator =
wenzelm@64703
   298
          for {
wenzelm@65232
   299
            (file, model, rendering) <- flushed.iterator
wenzelm@65115
   300
            (changed_diags, changed_decos, model1) = model.publish(rendering)
wenzelm@65115
   301
            if changed_diags.isDefined || changed_decos.isDefined
wenzelm@65095
   302
          }
wenzelm@65095
   303
          yield {
wenzelm@65115
   304
            for (diags <- changed_diags)
wenzelm@65115
   305
              channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
wenzelm@65137
   306
            if (pide_extensions) {
wenzelm@65137
   307
              for (decos <- changed_decos; deco <- decos)
wenzelm@65137
   308
                channel.write(rendering.decoration_output(deco).json(file))
wenzelm@65137
   309
            }
wenzelm@64777
   310
            (file, model1)
wenzelm@64703
   311
          }
wenzelm@65232
   312
wenzelm@65232
   313
        (postponed.nonEmpty,
wenzelm@65232
   314
          st.copy(
wenzelm@65232
   315
            models = st.models ++ changed_iterator,
wenzelm@65232
   316
            pending_output = postponed.map(_._1).toSet))
wenzelm@64703
   317
      }
wenzelm@64703
   318
    )
wenzelm@64703
   319
  }
wenzelm@64870
   320
wenzelm@64870
   321
wenzelm@64870
   322
  /* output text */
wenzelm@64870
   323
wenzelm@64870
   324
  def output_text(s: String): String =
wenzelm@65137
   325
    if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
wenzelm@64870
   326
wenzelm@65108
   327
  def output_xml(xml: XML.Tree): String =
wenzelm@65108
   328
    output_text(XML.content(xml))
wenzelm@65108
   329
wenzelm@64870
   330
  def output_pretty(body: XML.Body, margin: Int): String =
wenzelm@64870
   331
    output_text(Pretty.string_of(body, margin))
wenzelm@65108
   332
  def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
wenzelm@65108
   333
  def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
wenzelm@65142
   334
wenzelm@65142
   335
wenzelm@65189
   336
  /* caret handling */
wenzelm@65189
   337
wenzelm@65191
   338
  def update_caret(caret: Option[(JFile, Line.Position)])
wenzelm@65926
   339
  { state.change(_.update_caret(caret)) }
wenzelm@65189
   340
wenzelm@66086
   341
  def get_caret(): Option[VSCode_Resources.Caret] =
wenzelm@65189
   342
  {
wenzelm@65189
   343
    val st = state.value
wenzelm@65189
   344
    for {
wenzelm@65189
   345
      (file, pos) <- st.caret
wenzelm@65189
   346
      model <- st.models.get(file)
wenzelm@65191
   347
      offset <- model.content.doc.offset(pos)
wenzelm@65189
   348
    }
wenzelm@66086
   349
    yield VSCode_Resources.Caret(file, model, offset)
wenzelm@65189
   350
  }
wenzelm@65189
   351
wenzelm@65189
   352
wenzelm@65142
   353
  /* spell checker */
wenzelm@65142
   354
wenzelm@65142
   355
  val spell_checker = new Spell_Checker_Variable
wenzelm@65142
   356
  spell_checker.update(options)
wenzelm@64605
   357
}