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