src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Sun Jan 08 14:46:04 2017 +0100 (2017-01-08 ago)
changeset 64834 0a7179ad430d
parent 64833 0f410e3b1d20
child 64839 842163abfc0d
permissions -rw-r--r--
tuned;
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@64777
    24
    pending_output: Set[JFile] = Set.empty)
wenzelm@64800
    25
  {
wenzelm@64800
    26
    lazy val document_blobs: Document.Blobs =
wenzelm@64800
    27
      Document.Blobs(
wenzelm@64800
    28
        (for {
wenzelm@64800
    29
          (_, model) <- models.iterator
wenzelm@64800
    30
          blob <- model.get_blob
wenzelm@64800
    31
        } yield (model.node_name -> blob)).toMap)
wenzelm@64800
    32
  }
wenzelm@64605
    33
}
wenzelm@64605
    34
wenzelm@64624
    35
class VSCode_Resources(
wenzelm@64703
    36
    val options: Options,
wenzelm@64706
    37
    val text_length: Text.Length,
wenzelm@64605
    38
    loaded_theories: Set[String],
wenzelm@64605
    39
    known_theories: Map[String, Document.Node.Name],
wenzelm@64718
    40
    base_syntax: Outer_Syntax,
wenzelm@64718
    41
    log: Logger = No_Logger)
wenzelm@64718
    42
  extends Resources(loaded_theories, known_theories, base_syntax, log)
wenzelm@64605
    43
{
wenzelm@64703
    44
  private val state = Synchronized(VSCode_Resources.State())
wenzelm@64703
    45
wenzelm@64703
    46
wenzelm@64703
    47
  /* document node name */
wenzelm@64703
    48
wenzelm@64777
    49
  def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
wenzelm@64777
    50
wenzelm@64777
    51
  def node_name(file: JFile): Document.Node.Name =
wenzelm@64605
    52
  {
wenzelm@64777
    53
    val node = file.getPath
wenzelm@64777
    54
    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
wenzelm@64777
    55
    val master_dir = if (theory == "") "" else file.getParent
wenzelm@64777
    56
    Document.Node.Name(node, master_dir, theory)
wenzelm@64605
    57
  }
wenzelm@64703
    58
wenzelm@64759
    59
  override def append(dir: String, source_path: Path): String =
wenzelm@64716
    60
  {
wenzelm@64759
    61
    val path = source_path.expand
wenzelm@64777
    62
    if (dir == "" || path.is_absolute) File.platform_path(path)
wenzelm@64759
    63
    else if (path.is_current) dir
wenzelm@64777
    64
    else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
wenzelm@64777
    65
      dir + JFile.separator + File.platform_path(path)
wenzelm@64777
    66
    else if (path.is_basic) dir + File.platform_path(path)
wenzelm@64777
    67
    else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
wenzelm@64716
    68
  }
wenzelm@64716
    69
wenzelm@64834
    70
  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
wenzelm@64834
    71
  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
wenzelm@64834
    72
wenzelm@64834
    73
wenzelm@64834
    74
  /* file content */
wenzelm@64834
    75
wenzelm@64834
    76
  def read_file_content(file: JFile): Option[String] =
wenzelm@64834
    77
    try { Some(Line.normalize(File.read(file))) }
wenzelm@64834
    78
    catch { case ERROR(_) => None }
wenzelm@64834
    79
wenzelm@64834
    80
  def get_file_content(file: JFile): Option[String] =
wenzelm@64834
    81
    get_model(file) match {
wenzelm@64834
    82
      case Some(model) => Some(model.content.text)
wenzelm@64834
    83
      case None => read_file_content(file)
wenzelm@64834
    84
    }
wenzelm@64834
    85
wenzelm@64834
    86
  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
wenzelm@64834
    87
    for {
wenzelm@64834
    88
      (_, model) <- state.value.models.iterator
wenzelm@64834
    89
      Text.Info(range, entry) <- model.content.bibtex_entries.iterator
wenzelm@64834
    90
    } yield Text.Info(range, (entry, model))
wenzelm@64834
    91
wenzelm@64727
    92
  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
wenzelm@64727
    93
  {
wenzelm@64777
    94
    val file = node_file(name)
wenzelm@64777
    95
    get_model(file) match {
wenzelm@64830
    96
      case Some(model) => f(Scan.char_reader(model.content.text))
wenzelm@64777
    97
      case None if file.isFile =>
wenzelm@64727
    98
        val reader = Scan.byte_reader(file)
wenzelm@64727
    99
        try { f(reader) } finally { reader.close }
wenzelm@64777
   100
      case None =>
wenzelm@64777
   101
        error("No such file: " + quote(file.toString))
wenzelm@64727
   102
    }
wenzelm@64727
   103
  }
wenzelm@64727
   104
wenzelm@64703
   105
wenzelm@64703
   106
  /* document models */
wenzelm@64703
   107
wenzelm@64800
   108
  def visible_node(name: Document.Node.Name): Boolean =
wenzelm@64800
   109
    get_model(name) match {
wenzelm@64800
   110
      case Some(model) => model.node_visible
wenzelm@64800
   111
      case None => false
wenzelm@64800
   112
    }
wenzelm@64800
   113
wenzelm@64777
   114
  def update_model(session: Session, file: JFile, text: String)
wenzelm@64703
   115
  {
wenzelm@64703
   116
    state.change(st =>
wenzelm@64709
   117
      {
wenzelm@64777
   118
        val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
wenzelm@64727
   119
        val model1 = (model.update_text(text) getOrElse model).external(false)
wenzelm@64709
   120
        st.copy(
wenzelm@64777
   121
          models = st.models + (file -> model1),
wenzelm@64777
   122
          pending_input = st.pending_input + file)
wenzelm@64709
   123
      })
wenzelm@64703
   124
  }
wenzelm@64703
   125
wenzelm@64777
   126
  def close_model(file: JFile): Option[Document_Model] =
wenzelm@64710
   127
    state.change_result(st =>
wenzelm@64777
   128
      st.models.get(file) match {
wenzelm@64710
   129
        case None => (None, st)
wenzelm@64710
   130
        case Some(model) =>
wenzelm@64777
   131
          (Some(model), st.copy(models = st.models + (file -> model.external(true))))
wenzelm@64710
   132
      })
wenzelm@64710
   133
wenzelm@64722
   134
  def sync_models(changed_files: Set[JFile]): Boolean =
wenzelm@64710
   135
    state.change_result(st =>
wenzelm@64710
   136
      {
wenzelm@64719
   137
        val changed_models =
wenzelm@64710
   138
          (for {
wenzelm@64777
   139
            (file, model) <- st.models.iterator
wenzelm@64777
   140
            if changed_files(file) && model.external_file
wenzelm@64812
   141
            text <- read_file_content(file)
wenzelm@64779
   142
            model1 <- model.update_text(text)
wenzelm@64777
   143
          } yield (file, model1)).toList
wenzelm@64719
   144
        if (changed_models.isEmpty) (false, st)
wenzelm@64721
   145
        else (true,
wenzelm@64721
   146
          st.copy(
wenzelm@64721
   147
            models = (st.models /: changed_models)(_ + _),
wenzelm@64721
   148
            pending_input = (st.pending_input /: changed_models.iterator.map(_._1))(_ + _)))
wenzelm@64710
   149
      })
wenzelm@64710
   150
wenzelm@64703
   151
wenzelm@64727
   152
  /* resolve dependencies */
wenzelm@64727
   153
wenzelm@64731
   154
  val thy_info = new Thy_Info(this)
wenzelm@64731
   155
wenzelm@64800
   156
  def resolve_dependencies(session: Session, watcher: File_Watcher): (Boolean, Boolean) =
wenzelm@64727
   157
  {
wenzelm@64727
   158
    state.change_result(st =>
wenzelm@64727
   159
      {
wenzelm@64800
   160
        /* theory files */
wenzelm@64800
   161
wenzelm@64731
   162
        val thys =
wenzelm@64731
   163
          (for ((_, model) <- st.models.iterator if model.is_theory)
wenzelm@64731
   164
           yield (model.node_name, Position.none)).toList
wenzelm@64731
   165
wenzelm@64800
   166
        val thy_files = thy_info.dependencies("", thys).deps.map(_.name)
wenzelm@64800
   167
wenzelm@64800
   168
wenzelm@64800
   169
        /* auxiliary files */
wenzelm@64800
   170
wenzelm@64800
   171
        val stable_tip_version =
wenzelm@64815
   172
          if (st.models.forall(entry => entry._2.is_stable))
wenzelm@64800
   173
            session.current_state().stable_tip_version
wenzelm@64800
   174
          else None
wenzelm@64800
   175
wenzelm@64800
   176
        val aux_files =
wenzelm@64800
   177
          stable_tip_version match {
wenzelm@64800
   178
            case Some(version) => undefined_blobs(version.nodes)
wenzelm@64800
   179
            case None => Nil
wenzelm@64800
   180
          }
wenzelm@64800
   181
wenzelm@64800
   182
wenzelm@64800
   183
        /* loaded models */
wenzelm@64800
   184
wenzelm@64727
   185
        val loaded_models =
wenzelm@64731
   186
          (for {
wenzelm@64800
   187
            node_name <- thy_files.iterator ++ aux_files.iterator
wenzelm@64800
   188
            file = node_file(node_name)
wenzelm@64777
   189
            if !st.models.isDefinedAt(file)
wenzelm@64812
   190
            text <- { watcher.register_parent(file); read_file_content(file) }
wenzelm@64727
   191
          }
wenzelm@64727
   192
          yield {
wenzelm@64800
   193
            val model = Document_Model.init(session, node_name)
wenzelm@64727
   194
            val model1 = (model.update_text(text) getOrElse model).external(true)
wenzelm@64777
   195
            (file, model1)
wenzelm@64731
   196
          }).toList
wenzelm@64731
   197
wenzelm@64800
   198
        val invoke_input = loaded_models.nonEmpty
wenzelm@64800
   199
        val invoke_load = stable_tip_version.isEmpty
wenzelm@64800
   200
wenzelm@64800
   201
        ((invoke_input, invoke_load),
wenzelm@64800
   202
          st.copy(
wenzelm@64800
   203
            models = st.models ++ loaded_models,
wenzelm@64800
   204
            pending_input = st.pending_input ++ loaded_models.iterator.map(_._1)))
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@64777
   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@64777
   232
  def update_output(changed_nodes: List[JFile]): Unit =
wenzelm@64703
   233
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
wenzelm@64703
   234
wenzelm@64703
   235
  def flush_output(channel: Channel)
wenzelm@64703
   236
  {
wenzelm@64703
   237
    state.change(st =>
wenzelm@64703
   238
      {
wenzelm@64703
   239
        val changed_iterator =
wenzelm@64703
   240
          for {
wenzelm@64777
   241
            file <- st.pending_output.iterator
wenzelm@64777
   242
            model <- st.models.get(file)
wenzelm@64704
   243
            rendering = model.rendering()
wenzelm@64703
   244
            (diagnostics, model1) <- model.publish_diagnostics(rendering)
wenzelm@64703
   245
          } yield {
wenzelm@64777
   246
            channel.diagnostics(file, rendering.diagnostics_output(diagnostics))
wenzelm@64777
   247
            (file, model1)
wenzelm@64703
   248
          }
wenzelm@64703
   249
        st.copy(
wenzelm@64777
   250
          models = (st.models /: changed_iterator)(_ + _),
wenzelm@64703
   251
          pending_output = Set.empty)
wenzelm@64703
   252
      }
wenzelm@64703
   253
    )
wenzelm@64703
   254
  }
wenzelm@64605
   255
}