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