64623
|
1 |
/* Title: Tools/VSCode/src/vscode_resources.scala
|
64605
|
2 |
Author: Makarius
|
|
3 |
|
64623
|
4 |
Resources for VSCode Language Server, based on file-system URIs.
|
64605
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.vscode
|
|
8 |
|
|
9 |
|
|
10 |
import isabelle._
|
|
11 |
|
|
12 |
import java.net.{URI, URISyntaxException}
|
|
13 |
import java.io.{File => JFile}
|
|
14 |
|
|
15 |
|
64623
|
16 |
object VSCode_Resources
|
64605
|
17 |
{
|
64703
|
18 |
/* file URIs */
|
|
19 |
|
64605
|
20 |
def is_wellformed(uri: String): Boolean =
|
|
21 |
try { new JFile(new URI(uri)); true }
|
|
22 |
catch { case _: URISyntaxException | _: IllegalArgumentException => false }
|
|
23 |
|
|
24 |
def canonical_file(uri: String): JFile =
|
|
25 |
new JFile(new URI(uri)).getCanonicalFile
|
|
26 |
|
64703
|
27 |
|
|
28 |
/* internal state */
|
|
29 |
|
|
30 |
sealed case class State(
|
|
31 |
models: Map[String, Document_Model] = Map.empty,
|
|
32 |
pending_input: Set[Document.Node.Name] = Set.empty,
|
|
33 |
pending_output: Set[Document.Node.Name] = Set.empty)
|
64605
|
34 |
}
|
|
35 |
|
64623
|
36 |
class VSCode_Resources(
|
64703
|
37 |
val options: Options,
|
64605
|
38 |
loaded_theories: Set[String],
|
|
39 |
known_theories: Map[String, Document.Node.Name],
|
|
40 |
base_syntax: Outer_Syntax)
|
|
41 |
extends Resources(loaded_theories, known_theories, base_syntax)
|
|
42 |
{
|
64703
|
43 |
private val state = Synchronized(VSCode_Resources.State())
|
|
44 |
|
|
45 |
|
|
46 |
/* document node name */
|
|
47 |
|
64605
|
48 |
def node_name(uri: String): Document.Node.Name =
|
|
49 |
{
|
64640
|
50 |
val theory = Thy_Header.thy_name(uri).getOrElse("")
|
|
51 |
val master_dir =
|
|
52 |
if (!VSCode_Resources.is_wellformed(uri) || theory == "") ""
|
|
53 |
else VSCode_Resources.canonical_file(uri).getParent
|
|
54 |
Document.Node.Name(uri, master_dir, theory)
|
64605
|
55 |
}
|
64703
|
56 |
|
|
57 |
|
|
58 |
/* document models */
|
|
59 |
|
|
60 |
def get_model(uri: String): Option[Document_Model] = state.value.models.get(uri)
|
|
61 |
|
|
62 |
def update_model(model: Document_Model)
|
|
63 |
{
|
|
64 |
state.change(st =>
|
|
65 |
st.copy(
|
|
66 |
models = st.models + (model.node_name.node -> model),
|
|
67 |
pending_input = st.pending_input + model.node_name))
|
|
68 |
}
|
|
69 |
|
|
70 |
|
|
71 |
/* pending input */
|
|
72 |
|
|
73 |
def flush_input(session: Session)
|
|
74 |
{
|
|
75 |
state.change(st =>
|
|
76 |
{
|
|
77 |
val changed =
|
|
78 |
(for {
|
|
79 |
node_name <- st.pending_input.iterator
|
|
80 |
model <- st.models.get(node_name.node)
|
|
81 |
if model.changed } yield model).toList
|
|
82 |
val edits = for { model <- changed; edit <- model.node_edits } yield edit
|
|
83 |
session.update(Document.Blobs.empty, edits)
|
|
84 |
st.copy(
|
|
85 |
models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
|
|
86 |
pending_input = Set.empty)
|
|
87 |
})
|
|
88 |
}
|
|
89 |
|
|
90 |
|
|
91 |
/* pending output */
|
|
92 |
|
|
93 |
def update_output(changed_nodes: Set[Document.Node.Name]): Unit =
|
|
94 |
state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
|
|
95 |
|
|
96 |
def flush_output(channel: Channel)
|
|
97 |
{
|
|
98 |
state.change(st =>
|
|
99 |
{
|
|
100 |
val changed_iterator =
|
|
101 |
for {
|
|
102 |
node_name <- st.pending_output.iterator
|
|
103 |
model <- st.models.get(node_name.node)
|
|
104 |
rendering = model.rendering(options)
|
|
105 |
(diagnostics, model1) <- model.publish_diagnostics(rendering)
|
|
106 |
} yield {
|
|
107 |
channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
|
|
108 |
model1
|
|
109 |
}
|
|
110 |
st.copy(
|
|
111 |
models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
|
|
112 |
pending_output = Set.empty)
|
|
113 |
}
|
|
114 |
)
|
|
115 |
}
|
64605
|
116 |
}
|