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