src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Fri Apr 21 14:09:03 2017 +0200 (2017-04-21 ago)
changeset 65532 febfd9f78bd4
parent 65524 0910f1733909
child 65926 0f7821a07aa9
permissions -rw-r--r--
eliminated default_qualifier: just a constant;
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@64777
    23
    pending_input: Set[JFile] = Set.empty,
wenzelm@65189
    24
    pending_output: Set[JFile] = Set.empty,
wenzelm@65189
    25
    caret: Option[(JFile, Line.Position)] = None)
wenzelm@64800
    26
  {
wenzelm@65113
    27
    def update_models(changed: Traversable[(JFile, Document_Model)]): State =
wenzelm@65111
    28
      copy(
wenzelm@65113
    29
        models = models ++ changed,
wenzelm@65113
    30
        pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
wenzelm@65113
    31
        pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file })
wenzelm@65111
    32
wenzelm@64800
    33
    lazy val document_blobs: Document.Blobs =
wenzelm@64800
    34
      Document.Blobs(
wenzelm@64800
    35
        (for {
wenzelm@64800
    36
          (_, model) <- models.iterator
wenzelm@64800
    37
          blob <- model.get_blob
wenzelm@64800
    38
        } yield (model.node_name -> blob)).toMap)
wenzelm@64800
    39
  }
wenzelm@64605
    40
}
wenzelm@64605
    41
wenzelm@64624
    42
class VSCode_Resources(
wenzelm@65361
    43
    val options: Options,
wenzelm@65361
    44
    session_base: Sessions.Base,
wenzelm@65361
    45
    log: Logger = No_Logger)
wenzelm@65441
    46
  extends Resources(session_base, log = log)
wenzelm@64605
    47
{
wenzelm@64703
    48
  private val state = Synchronized(VSCode_Resources.State())
wenzelm@64703
    49
wenzelm@64703
    50
wenzelm@65137
    51
  /* options */
wenzelm@65137
    52
wenzelm@65137
    53
  def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
wenzelm@65137
    54
  def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
wenzelm@65137
    55
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
wenzelm@65137
    56
  def message_margin: Int = options.int("vscode_message_margin")
wenzelm@65137
    57
wenzelm@65137
    58
wenzelm@64703
    59
  /* document node name */
wenzelm@64703
    60
wenzelm@64777
    61
  def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
wenzelm@64777
    62
wenzelm@64777
    63
  def node_name(file: JFile): Document.Node.Name =
wenzelm@65524
    64
    session_base.known.get_file(file) getOrElse {
wenzelm@65501
    65
      val node = file.getPath
wenzelm@65532
    66
      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
wenzelm@65501
    67
        case (true, theory) => Document.Node.Name.loaded_theory(theory)
wenzelm@65501
    68
        case (false, theory) =>
wenzelm@65501
    69
          val master_dir = if (theory == "") "" else file.getParent
wenzelm@65501
    70
          Document.Node.Name(node, master_dir, theory)
wenzelm@65501
    71
      }
wenzelm@65472
    72
    }
wenzelm@64703
    73
wenzelm@64759
    74
  override def append(dir: String, source_path: Path): String =
wenzelm@64716
    75
  {
wenzelm@64759
    76
    val path = source_path.expand
wenzelm@64777
    77
    if (dir == "" || path.is_absolute) File.platform_path(path)
wenzelm@64759
    78
    else if (path.is_current) dir
wenzelm@64777
    79
    else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
wenzelm@64777
    80
      dir + JFile.separator + File.platform_path(path)
wenzelm@64777
    81
    else if (path.is_basic) dir + File.platform_path(path)
wenzelm@64777
    82
    else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
wenzelm@64716
    83
  }
wenzelm@64716
    84
wenzelm@64834
    85
  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
wenzelm@64834
    86
  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
wenzelm@64834
    87
wenzelm@64834
    88
wenzelm@64834
    89
  /* file content */
wenzelm@64834
    90
wenzelm@64834
    91
  def read_file_content(file: JFile): Option[String] =
wenzelm@64834
    92
    try { Some(Line.normalize(File.read(file))) }
wenzelm@64834
    93
    catch { case ERROR(_) => None }
wenzelm@64834
    94
wenzelm@64834
    95
  def get_file_content(file: JFile): Option[String] =
wenzelm@64834
    96
    get_model(file) match {
wenzelm@64834
    97
      case Some(model) => Some(model.content.text)
wenzelm@64834
    98
      case None => read_file_content(file)
wenzelm@64834
    99
    }
wenzelm@64834
   100
wenzelm@64834
   101
  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
wenzelm@64834
   102
    for {
wenzelm@64834
   103
      (_, model) <- state.value.models.iterator
wenzelm@65132
   104
      info <- model.content.bibtex_entries.iterator
wenzelm@65132
   105
    } yield info.map((_, model))
wenzelm@64834
   106
wenzelm@64727
   107
  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
wenzelm@64727
   108
  {
wenzelm@64777
   109
    val file = node_file(name)
wenzelm@64777
   110
    get_model(file) match {
wenzelm@64830
   111
      case Some(model) => f(Scan.char_reader(model.content.text))
wenzelm@64777
   112
      case None if file.isFile =>
wenzelm@64727
   113
        val reader = Scan.byte_reader(file)
wenzelm@64727
   114
        try { f(reader) } finally { reader.close }
wenzelm@64777
   115
      case None =>
wenzelm@64777
   116
        error("No such file: " + quote(file.toString))
wenzelm@64727
   117
    }
wenzelm@64727
   118
  }
wenzelm@64727
   119
wenzelm@64703
   120
wenzelm@64703
   121
  /* document models */
wenzelm@64703
   122
wenzelm@64800
   123
  def visible_node(name: Document.Node.Name): Boolean =
wenzelm@64800
   124
    get_model(name) match {
wenzelm@64800
   125
      case Some(model) => model.node_visible
wenzelm@64800
   126
      case None => false
wenzelm@64800
   127
    }
wenzelm@64800
   128
wenzelm@65160
   129
  def change_model(session: Session, file: JFile, text: String, range: Option[Line.Range] = None)
wenzelm@64703
   130
  {
wenzelm@64703
   131
    state.change(st =>
wenzelm@64709
   132
      {
wenzelm@64777
   133
        val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
wenzelm@65160
   134
        val model1 = (model.change_text(text, range) getOrElse model).external(false)
wenzelm@65114
   135
        st.update_models(Some(file -> model1))
wenzelm@64709
   136
      })
wenzelm@64703
   137
  }
wenzelm@64703
   138
wenzelm@65111
   139
  def close_model(file: JFile): Boolean =
wenzelm@64710
   140
    state.change_result(st =>
wenzelm@64777
   141
      st.models.get(file) match {
wenzelm@65111
   142
        case None => (false, st)
wenzelm@65113
   143
        case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
wenzelm@64710
   144
      })
wenzelm@64710
   145
wenzelm@65116
   146
  def sync_models(changed_files: Set[JFile]): Unit =
wenzelm@65116
   147
    state.change(st =>
wenzelm@64710
   148
      {
wenzelm@64719
   149
        val changed_models =
wenzelm@64710
   150
          (for {
wenzelm@64777
   151
            (file, model) <- st.models.iterator
wenzelm@64777
   152
            if changed_files(file) && model.external_file
wenzelm@64812
   153
            text <- read_file_content(file)
wenzelm@65160
   154
            model1 <- model.change_text(text)
wenzelm@65116
   155
          } yield (file, model1)).toList
wenzelm@65116
   156
        st.update_models(changed_models)
wenzelm@64710
   157
      })
wenzelm@64710
   158
wenzelm@64703
   159
wenzelm@64727
   160
  /* resolve dependencies */
wenzelm@64727
   161
wenzelm@64857
   162
  def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) =
wenzelm@64727
   163
  {
wenzelm@64727
   164
    state.change_result(st =>
wenzelm@64727
   165
      {
wenzelm@64800
   166
        /* theory files */
wenzelm@64800
   167
wenzelm@64731
   168
        val thys =
wenzelm@64731
   169
          (for ((_, model) <- st.models.iterator if model.is_theory)
wenzelm@64731
   170
           yield (model.node_name, Position.none)).toList
wenzelm@64731
   171
wenzelm@65359
   172
        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
wenzelm@64800
   173
wenzelm@64800
   174
wenzelm@64800
   175
        /* auxiliary files */
wenzelm@64800
   176
wenzelm@64800
   177
        val stable_tip_version =
wenzelm@64815
   178
          if (st.models.forall(entry => entry._2.is_stable))
wenzelm@64800
   179
            session.current_state().stable_tip_version
wenzelm@64800
   180
          else None
wenzelm@64800
   181
wenzelm@64800
   182
        val aux_files =
wenzelm@64800
   183
          stable_tip_version match {
wenzelm@64800
   184
            case Some(version) => undefined_blobs(version.nodes)
wenzelm@64800
   185
            case None => Nil
wenzelm@64800
   186
          }
wenzelm@64800
   187
wenzelm@64800
   188
wenzelm@64800
   189
        /* loaded models */
wenzelm@64800
   190
wenzelm@64727
   191
        val loaded_models =
wenzelm@64731
   192
          (for {
wenzelm@64800
   193
            node_name <- thy_files.iterator ++ aux_files.iterator
wenzelm@64800
   194
            file = node_file(node_name)
wenzelm@64777
   195
            if !st.models.isDefinedAt(file)
wenzelm@64857
   196
            text <- { file_watcher.register_parent(file); read_file_content(file) }
wenzelm@64727
   197
          }
wenzelm@64727
   198
          yield {
wenzelm@64800
   199
            val model = Document_Model.init(session, node_name)
wenzelm@65160
   200
            val model1 = (model.change_text(text) getOrElse model).external(true)
wenzelm@64777
   201
            (file, model1)
wenzelm@65117
   202
          }).toList
wenzelm@64731
   203
wenzelm@64800
   204
        val invoke_input = loaded_models.nonEmpty
wenzelm@64800
   205
        val invoke_load = stable_tip_version.isEmpty
wenzelm@64800
   206
wenzelm@65113
   207
        ((invoke_input, invoke_load), st.update_models(loaded_models))
wenzelm@64727
   208
      })
wenzelm@64727
   209
  }
wenzelm@64727
   210
wenzelm@64727
   211
wenzelm@64703
   212
  /* pending input */
wenzelm@64703
   213
wenzelm@64703
   214
  def flush_input(session: Session)
wenzelm@64703
   215
  {
wenzelm@64703
   216
    state.change(st =>
wenzelm@64703
   217
      {
wenzelm@64719
   218
        val changed_models =
wenzelm@64703
   219
          (for {
wenzelm@64777
   220
            file <- st.pending_input.iterator
wenzelm@64777
   221
            model <- st.models.get(file)
wenzelm@64800
   222
            (edits, model1) <- model.flush_edits(st.document_blobs)
wenzelm@64777
   223
          } yield (edits, (file, model1))).toList
wenzelm@64707
   224
wenzelm@64800
   225
        session.update(st.document_blobs, changed_models.flatMap(_._1))
wenzelm@64703
   226
        st.copy(
wenzelm@65112
   227
          models = st.models ++ changed_models.iterator.map(_._2),
wenzelm@64703
   228
          pending_input = Set.empty)
wenzelm@64703
   229
      })
wenzelm@64703
   230
  }
wenzelm@64703
   231
wenzelm@64703
   232
wenzelm@64703
   233
  /* pending output */
wenzelm@64703
   234
wenzelm@65118
   235
  def update_output(changed_nodes: Traversable[JFile]): Unit =
wenzelm@64703
   236
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
wenzelm@64703
   237
wenzelm@65232
   238
  def flush_output(channel: Channel): Boolean =
wenzelm@64703
   239
  {
wenzelm@65232
   240
    state.change_result(st =>
wenzelm@64703
   241
      {
wenzelm@65232
   242
        val (postponed, flushed) =
wenzelm@65232
   243
          (for {
wenzelm@65232
   244
            file <- st.pending_output.iterator
wenzelm@65232
   245
            model <- st.models.get(file)
wenzelm@65232
   246
          } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
wenzelm@65232
   247
wenzelm@64703
   248
        val changed_iterator =
wenzelm@64703
   249
          for {
wenzelm@65232
   250
            (file, model, rendering) <- flushed.iterator
wenzelm@65115
   251
            (changed_diags, changed_decos, model1) = model.publish(rendering)
wenzelm@65115
   252
            if changed_diags.isDefined || changed_decos.isDefined
wenzelm@65095
   253
          }
wenzelm@65095
   254
          yield {
wenzelm@65115
   255
            for (diags <- changed_diags)
wenzelm@65115
   256
              channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
wenzelm@65137
   257
            if (pide_extensions) {
wenzelm@65137
   258
              for (decos <- changed_decos; deco <- decos)
wenzelm@65137
   259
                channel.write(rendering.decoration_output(deco).json(file))
wenzelm@65137
   260
            }
wenzelm@64777
   261
            (file, model1)
wenzelm@64703
   262
          }
wenzelm@65232
   263
wenzelm@65232
   264
        (postponed.nonEmpty,
wenzelm@65232
   265
          st.copy(
wenzelm@65232
   266
            models = st.models ++ changed_iterator,
wenzelm@65232
   267
            pending_output = postponed.map(_._1).toSet))
wenzelm@64703
   268
      }
wenzelm@64703
   269
    )
wenzelm@64703
   270
  }
wenzelm@64870
   271
wenzelm@64870
   272
wenzelm@64870
   273
  /* output text */
wenzelm@64870
   274
wenzelm@64870
   275
  def output_text(s: String): String =
wenzelm@65137
   276
    if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
wenzelm@64870
   277
wenzelm@65108
   278
  def output_xml(xml: XML.Tree): String =
wenzelm@65108
   279
    output_text(XML.content(xml))
wenzelm@65108
   280
wenzelm@64870
   281
  def output_pretty(body: XML.Body, margin: Int): String =
wenzelm@64870
   282
    output_text(Pretty.string_of(body, margin))
wenzelm@65108
   283
  def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
wenzelm@65108
   284
  def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
wenzelm@65142
   285
wenzelm@65142
   286
wenzelm@65189
   287
  /* caret handling */
wenzelm@65189
   288
wenzelm@65191
   289
  def update_caret(caret: Option[(JFile, Line.Position)])
wenzelm@65191
   290
  { state.change(_.copy(caret = caret)) }
wenzelm@65189
   291
wenzelm@65198
   292
  def caret_offset(): Option[(Document_Model, Text.Offset)] =
wenzelm@65189
   293
  {
wenzelm@65189
   294
    val st = state.value
wenzelm@65189
   295
    for {
wenzelm@65189
   296
      (file, pos) <- st.caret
wenzelm@65189
   297
      model <- st.models.get(file)
wenzelm@65191
   298
      offset <- model.content.doc.offset(pos)
wenzelm@65189
   299
    }
wenzelm@65198
   300
    yield (model, offset)
wenzelm@65189
   301
  }
wenzelm@65189
   302
wenzelm@65189
   303
wenzelm@65142
   304
  /* spell checker */
wenzelm@65142
   305
wenzelm@65142
   306
  val spell_checker = new Spell_Checker_Variable
wenzelm@65142
   307
  spell_checker.update(options)
wenzelm@64605
   308
}