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,
|
64708
|
32 |
pending_input: Set[String] = Set.empty,
|
|
33 |
pending_output: Set[String] = Set.empty)
|
64605
|
34 |
}
|
|
35 |
|
64623
|
36 |
class VSCode_Resources(
|
64703
|
37 |
val options: Options,
|
64706
|
38 |
val text_length: Text.Length,
|
64605
|
39 |
loaded_theories: Set[String],
|
|
40 |
known_theories: Map[String, Document.Node.Name],
|
64718
|
41 |
base_syntax: Outer_Syntax,
|
|
42 |
log: Logger = No_Logger)
|
|
43 |
extends Resources(loaded_theories, known_theories, base_syntax, log)
|
64605
|
44 |
{
|
64703
|
45 |
private val state = Synchronized(VSCode_Resources.State())
|
|
46 |
|
|
47 |
|
|
48 |
/* document node name */
|
|
49 |
|
64605
|
50 |
def node_name(uri: String): Document.Node.Name =
|
|
51 |
{
|
64640
|
52 |
val theory = Thy_Header.thy_name(uri).getOrElse("")
|
|
53 |
val master_dir =
|
|
54 |
if (!VSCode_Resources.is_wellformed(uri) || theory == "") ""
|
|
55 |
else VSCode_Resources.canonical_file(uri).getParent
|
|
56 |
Document.Node.Name(uri, master_dir, theory)
|
64605
|
57 |
}
|
64703
|
58 |
|
64716
|
59 |
override def import_name(qualifier: String, master: Document.Node.Name, s: String)
|
|
60 |
: Document.Node.Name =
|
|
61 |
{
|
|
62 |
val name = super.import_name(qualifier, master, s)
|
|
63 |
if (name.node.startsWith("file://") || name.node.forall(c => c != '/' && c != '\\')) name
|
|
64 |
else name.copy(node = "file://" + name.node)
|
|
65 |
}
|
|
66 |
|
64703
|
67 |
|
|
68 |
/* document models */
|
|
69 |
|
|
70 |
def get_model(uri: String): Option[Document_Model] = state.value.models.get(uri)
|
|
71 |
|
64709
|
72 |
def update_model(session: Session, uri: String, text: String)
|
64703
|
73 |
{
|
|
74 |
state.change(st =>
|
64709
|
75 |
{
|
64710
|
76 |
val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
|
|
77 |
val model1 = (model.update_text(text) getOrElse model).copy(external = false)
|
64709
|
78 |
st.copy(
|
64710
|
79 |
models = st.models + (uri -> model1),
|
64709
|
80 |
pending_input = st.pending_input + uri)
|
|
81 |
})
|
64703
|
82 |
}
|
|
83 |
|
64710
|
84 |
def close_model(uri: String): Option[Document_Model] =
|
|
85 |
state.change_result(st =>
|
|
86 |
st.models.get(uri) match {
|
|
87 |
case None => (None, st)
|
|
88 |
case Some(model) =>
|
|
89 |
(Some(model), st.copy(models = st.models + (uri -> model.copy(external = true))))
|
|
90 |
})
|
|
91 |
|
|
92 |
def sync_external(changed_files: Set[JFile]): Boolean =
|
|
93 |
state.change_result(st =>
|
|
94 |
{
|
64719
|
95 |
val changed_models =
|
64710
|
96 |
(for {
|
|
97 |
(uri, model) <- st.models.iterator
|
|
98 |
if changed_files(model.file)
|
|
99 |
model1 <- model.update_file
|
64721
|
100 |
} yield (uri, model1)).toList
|
64719
|
101 |
if (changed_models.isEmpty) (false, st)
|
64721
|
102 |
else (true,
|
|
103 |
st.copy(
|
|
104 |
models = (st.models /: changed_models)(_ + _),
|
|
105 |
pending_input = (st.pending_input /: changed_models.iterator.map(_._1))(_ + _)))
|
64710
|
106 |
})
|
|
107 |
|
64703
|
108 |
|
|
109 |
/* pending input */
|
|
110 |
|
|
111 |
def flush_input(session: Session)
|
|
112 |
{
|
|
113 |
state.change(st =>
|
|
114 |
{
|
64719
|
115 |
val changed_models =
|
64703
|
116 |
(for {
|
64708
|
117 |
uri <- st.pending_input.iterator
|
|
118 |
model <- st.models.get(uri)
|
64707
|
119 |
res <- model.flush_edits
|
|
120 |
} yield res).toList
|
|
121 |
|
64719
|
122 |
session.update(Document.Blobs.empty, changed_models.flatMap(_._1))
|
64703
|
123 |
st.copy(
|
64719
|
124 |
models = (st.models /: changed_models) { case (ms, (_, m)) => ms + (m.uri -> m) },
|
64703
|
125 |
pending_input = Set.empty)
|
|
126 |
})
|
|
127 |
}
|
|
128 |
|
|
129 |
|
|
130 |
/* pending output */
|
|
131 |
|
64708
|
132 |
def update_output(changed_nodes: List[String]): Unit =
|
64703
|
133 |
state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
|
|
134 |
|
|
135 |
def flush_output(channel: Channel)
|
|
136 |
{
|
|
137 |
state.change(st =>
|
|
138 |
{
|
|
139 |
val changed_iterator =
|
|
140 |
for {
|
64708
|
141 |
uri <- st.pending_output.iterator
|
|
142 |
model <- st.models.get(uri)
|
64704
|
143 |
rendering = model.rendering()
|
64703
|
144 |
(diagnostics, model1) <- model.publish_diagnostics(rendering)
|
|
145 |
} yield {
|
|
146 |
channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
|
|
147 |
model1
|
|
148 |
}
|
|
149 |
st.copy(
|
|
150 |
models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
|
|
151 |
pending_output = Set.empty)
|
|
152 |
}
|
|
153 |
)
|
|
154 |
}
|
64605
|
155 |
}
|