author | wenzelm |
Fri, 21 Apr 2017 14:09:03 +0200 | |
changeset 65532 | febfd9f78bd4 |
parent 65524 | 0910f1733909 |
child 65926 | 0f7821a07aa9 |
permissions | -rw-r--r-- |
64623 | 1 |
/* Title: Tools/VSCode/src/vscode_resources.scala |
64605 | 2 |
Author: Makarius |
3 |
||
64729 | 4 |
Resources for VSCode Language Server: file-system access and global state. |
64605 | 5 |
*/ |
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import java.io.{File => JFile} |
|
13 |
||
64824 | 14 |
import scala.util.parsing.input.Reader |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
15 |
|
64605 | 16 |
|
64623 | 17 |
object VSCode_Resources |
64605 | 18 |
{ |
64703 | 19 |
/* internal state */ |
20 |
||
21 |
sealed case class State( |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
22 |
models: Map[JFile, Document_Model] = Map.empty, |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
23 |
pending_input: Set[JFile] = Set.empty, |
65189 | 24 |
pending_output: Set[JFile] = Set.empty, |
25 |
caret: Option[(JFile, Line.Position)] = None) |
|
64800 | 26 |
{ |
65113 | 27 |
def update_models(changed: Traversable[(JFile, Document_Model)]): State = |
65111
3224a6f7bd6b
more robust treatment of pending input/output: these are often correlated;
wenzelm
parents:
65107
diff
changeset
|
28 |
copy( |
65113 | 29 |
models = models ++ changed, |
30 |
pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file }, |
|
31 |
pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file }) |
|
65111
3224a6f7bd6b
more robust treatment of pending input/output: these are often correlated;
wenzelm
parents:
65107
diff
changeset
|
32 |
|
64800 | 33 |
lazy val document_blobs: Document.Blobs = |
34 |
Document.Blobs( |
|
35 |
(for { |
|
36 |
(_, model) <- models.iterator |
|
37 |
blob <- model.get_blob |
|
38 |
} yield (model.node_name -> blob)).toMap) |
|
39 |
} |
|
64605 | 40 |
} |
41 |
||
64623 | 42 |
class VSCode_Resources( |
65361 | 43 |
val options: Options, |
44 |
session_base: Sessions.Base, |
|
45 |
log: Logger = No_Logger) |
|
65441 | 46 |
extends Resources(session_base, log = log) |
64605 | 47 |
{ |
64703 | 48 |
private val state = Synchronized(VSCode_Resources.State()) |
49 |
||
50 |
||
65137 | 51 |
/* options */ |
52 |
||
53 |
def pide_extensions: Boolean = options.bool("vscode_pide_extensions") |
|
54 |
def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols") |
|
55 |
def tooltip_margin: Int = options.int("vscode_tooltip_margin") |
|
56 |
def message_margin: Int = options.int("vscode_message_margin") |
|
57 |
||
58 |
||
64703 | 59 |
/* document node name */ |
60 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
61 |
def node_file(name: Document.Node.Name): JFile = new JFile(name.node) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
62 |
|
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
63 |
def node_name(file: JFile): Document.Node.Name = |
65524 | 64 |
session_base.known.get_file(file) getOrElse { |
65501
b42743f5b595
prefer formal name from session context, for proper qualified theory name;
wenzelm
parents:
65476
diff
changeset
|
65 |
val node = file.getPath |
65532 | 66 |
theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match { |
65501
b42743f5b595
prefer formal name from session context, for proper qualified theory name;
wenzelm
parents:
65476
diff
changeset
|
67 |
case (true, theory) => Document.Node.Name.loaded_theory(theory) |
b42743f5b595
prefer formal name from session context, for proper qualified theory name;
wenzelm
parents:
65476
diff
changeset
|
68 |
case (false, theory) => |
b42743f5b595
prefer formal name from session context, for proper qualified theory name;
wenzelm
parents:
65476
diff
changeset
|
69 |
val master_dir = if (theory == "") "" else file.getParent |
b42743f5b595
prefer formal name from session context, for proper qualified theory name;
wenzelm
parents:
65476
diff
changeset
|
70 |
Document.Node.Name(node, master_dir, theory) |
b42743f5b595
prefer formal name from session context, for proper qualified theory name;
wenzelm
parents:
65476
diff
changeset
|
71 |
} |
65472 | 72 |
} |
64703 | 73 |
|
64759 | 74 |
override def append(dir: String, source_path: Path): String = |
64716 | 75 |
{ |
64759 | 76 |
val path = source_path.expand |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
77 |
if (dir == "" || path.is_absolute) File.platform_path(path) |
64759 | 78 |
else if (path.is_current) dir |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
79 |
else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator)) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
80 |
dir + JFile.separator + File.platform_path(path) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
81 |
else if (path.is_basic) dir + File.platform_path(path) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
82 |
else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath |
64716 | 83 |
} |
84 |
||
64834 | 85 |
def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file) |
86 |
def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name)) |
|
87 |
||
88 |
||
89 |
/* file content */ |
|
90 |
||
91 |
def read_file_content(file: JFile): Option[String] = |
|
92 |
try { Some(Line.normalize(File.read(file))) } |
|
93 |
catch { case ERROR(_) => None } |
|
94 |
||
95 |
def get_file_content(file: JFile): Option[String] = |
|
96 |
get_model(file) match { |
|
97 |
case Some(model) => Some(model.content.text) |
|
98 |
case None => read_file_content(file) |
|
99 |
} |
|
100 |
||
101 |
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = |
|
102 |
for { |
|
103 |
(_, model) <- state.value.models.iterator |
|
65132 | 104 |
info <- model.content.bibtex_entries.iterator |
105 |
} yield info.map((_, model)) |
|
64834 | 106 |
|
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
107 |
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
108 |
{ |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
109 |
val file = node_file(name) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
110 |
get_model(file) match { |
64830 | 111 |
case Some(model) => f(Scan.char_reader(model.content.text)) |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
112 |
case None if file.isFile => |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
113 |
val reader = Scan.byte_reader(file) |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
114 |
try { f(reader) } finally { reader.close } |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
115 |
case None => |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
116 |
error("No such file: " + quote(file.toString)) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
117 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
118 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
119 |
|
64703 | 120 |
|
121 |
/* document models */ |
|
122 |
||
64800 | 123 |
def visible_node(name: Document.Node.Name): Boolean = |
124 |
get_model(name) match { |
|
125 |
case Some(model) => model.node_visible |
|
126 |
case None => false |
|
127 |
} |
|
128 |
||
65160 | 129 |
def change_model(session: Session, file: JFile, text: String, range: Option[Line.Range] = None) |
64703 | 130 |
{ |
131 |
state.change(st => |
|
64709 | 132 |
{ |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
133 |
val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file))) |
65160 | 134 |
val model1 = (model.change_text(text, range) getOrElse model).external(false) |
65114
200b787ceb51
potentially redundant pending_output, for the sake of uniformity and reactivity;
wenzelm
parents:
65113
diff
changeset
|
135 |
st.update_models(Some(file -> model1)) |
64709 | 136 |
}) |
64703 | 137 |
} |
138 |
||
65111
3224a6f7bd6b
more robust treatment of pending input/output: these are often correlated;
wenzelm
parents:
65107
diff
changeset
|
139 |
def close_model(file: JFile): Boolean = |
64710 | 140 |
state.change_result(st => |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
141 |
st.models.get(file) match { |
65111
3224a6f7bd6b
more robust treatment of pending input/output: these are often correlated;
wenzelm
parents:
65107
diff
changeset
|
142 |
case None => (false, st) |
65113 | 143 |
case Some(model) => (true, st.update_models(Some(file -> model.external(true)))) |
64710 | 144 |
}) |
145 |
||
65116 | 146 |
def sync_models(changed_files: Set[JFile]): Unit = |
147 |
state.change(st => |
|
64710 | 148 |
{ |
64719 | 149 |
val changed_models = |
64710 | 150 |
(for { |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
151 |
(file, model) <- st.models.iterator |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
152 |
if changed_files(file) && model.external_file |
64812 | 153 |
text <- read_file_content(file) |
65160 | 154 |
model1 <- model.change_text(text) |
65116 | 155 |
} yield (file, model1)).toList |
156 |
st.update_models(changed_models) |
|
64710 | 157 |
}) |
158 |
||
64703 | 159 |
|
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
160 |
/* resolve dependencies */ |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
161 |
|
64857 | 162 |
def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) = |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
163 |
{ |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
164 |
state.change_result(st => |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
165 |
{ |
64800 | 166 |
/* theory files */ |
167 |
||
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
168 |
val thys = |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
169 |
(for ((_, model) <- st.models.iterator if model.is_theory) |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
170 |
yield (model.node_name, Position.none)).toList |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
171 |
|
65359 | 172 |
val thy_files = thy_info.dependencies(thys).deps.map(_.name) |
64800 | 173 |
|
174 |
||
175 |
/* auxiliary files */ |
|
176 |
||
177 |
val stable_tip_version = |
|
64815 | 178 |
if (st.models.forall(entry => entry._2.is_stable)) |
64800 | 179 |
session.current_state().stable_tip_version |
180 |
else None |
|
181 |
||
182 |
val aux_files = |
|
183 |
stable_tip_version match { |
|
184 |
case Some(version) => undefined_blobs(version.nodes) |
|
185 |
case None => Nil |
|
186 |
} |
|
187 |
||
188 |
||
189 |
/* loaded models */ |
|
190 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
191 |
val loaded_models = |
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
192 |
(for { |
64800 | 193 |
node_name <- thy_files.iterator ++ aux_files.iterator |
194 |
file = node_file(node_name) |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
195 |
if !st.models.isDefinedAt(file) |
64857 | 196 |
text <- { file_watcher.register_parent(file); read_file_content(file) } |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
197 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
198 |
yield { |
64800 | 199 |
val model = Document_Model.init(session, node_name) |
65160 | 200 |
val model1 = (model.change_text(text) getOrElse model).external(true) |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
201 |
(file, model1) |
65117 | 202 |
}).toList |
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
203 |
|
64800 | 204 |
val invoke_input = loaded_models.nonEmpty |
205 |
val invoke_load = stable_tip_version.isEmpty |
|
206 |
||
65113 | 207 |
((invoke_input, invoke_load), st.update_models(loaded_models)) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
208 |
}) |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
209 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
210 |
|
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
211 |
|
64703 | 212 |
/* pending input */ |
213 |
||
214 |
def flush_input(session: Session) |
|
215 |
{ |
|
216 |
state.change(st => |
|
217 |
{ |
|
64719 | 218 |
val changed_models = |
64703 | 219 |
(for { |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
220 |
file <- st.pending_input.iterator |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
221 |
model <- st.models.get(file) |
64800 | 222 |
(edits, model1) <- model.flush_edits(st.document_blobs) |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
223 |
} yield (edits, (file, model1))).toList |
64707 | 224 |
|
64800 | 225 |
session.update(st.document_blobs, changed_models.flatMap(_._1)) |
64703 | 226 |
st.copy( |
65112 | 227 |
models = st.models ++ changed_models.iterator.map(_._2), |
64703 | 228 |
pending_input = Set.empty) |
229 |
}) |
|
230 |
} |
|
231 |
||
232 |
||
233 |
/* pending output */ |
|
234 |
||
65118 | 235 |
def update_output(changed_nodes: Traversable[JFile]): Unit = |
64703 | 236 |
state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) |
237 |
||
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
238 |
def flush_output(channel: Channel): Boolean = |
64703 | 239 |
{ |
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
240 |
state.change_result(st => |
64703 | 241 |
{ |
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
242 |
val (postponed, flushed) = |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
243 |
(for { |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
244 |
file <- st.pending_output.iterator |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
245 |
model <- st.models.get(file) |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
246 |
} yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated) |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
247 |
|
64703 | 248 |
val changed_iterator = |
249 |
for { |
|
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
250 |
(file, model, rendering) <- flushed.iterator |
65115 | 251 |
(changed_diags, changed_decos, model1) = model.publish(rendering) |
252 |
if changed_diags.isDefined || changed_decos.isDefined |
|
65095 | 253 |
} |
254 |
yield { |
|
65115 | 255 |
for (diags <- changed_diags) |
256 |
channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags))) |
|
65137 | 257 |
if (pide_extensions) { |
258 |
for (decos <- changed_decos; deco <- decos) |
|
259 |
channel.write(rendering.decoration_output(deco).json(file)) |
|
260 |
} |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
261 |
(file, model1) |
64703 | 262 |
} |
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
263 |
|
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
264 |
(postponed.nonEmpty, |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
265 |
st.copy( |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
266 |
models = st.models ++ changed_iterator, |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
267 |
pending_output = postponed.map(_._1).toSet)) |
64703 | 268 |
} |
269 |
) |
|
270 |
} |
|
64870 | 271 |
|
272 |
||
273 |
/* output text */ |
|
274 |
||
275 |
def output_text(s: String): String = |
|
65137 | 276 |
if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |
64870 | 277 |
|
65107 | 278 |
def output_xml(xml: XML.Tree): String = |
279 |
output_text(XML.content(xml)) |
|
280 |
||
64870 | 281 |
def output_pretty(body: XML.Body, margin: Int): String = |
282 |
output_text(Pretty.string_of(body, margin)) |
|
65107 | 283 |
def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) |
284 |
def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) |
|
65142 | 285 |
|
286 |
||
65189 | 287 |
/* caret handling */ |
288 |
||
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
289 |
def update_caret(caret: Option[(JFile, Line.Position)]) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
290 |
{ state.change(_.copy(caret = caret)) } |
65189 | 291 |
|
65198 | 292 |
def caret_offset(): Option[(Document_Model, Text.Offset)] = |
65189 | 293 |
{ |
294 |
val st = state.value |
|
295 |
for { |
|
296 |
(file, pos) <- st.caret |
|
297 |
model <- st.models.get(file) |
|
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
298 |
offset <- model.content.doc.offset(pos) |
65189 | 299 |
} |
65198 | 300 |
yield (model, offset) |
65189 | 301 |
} |
302 |
||
303 |
||
65142 | 304 |
/* spell checker */ |
305 |
||
306 |
val spell_checker = new Spell_Checker_Variable |
|
307 |
spell_checker.update(options) |
|
64605 | 308 |
} |