--- a/src/Tools/VSCode/src/vscode_resources.scala Thu May 16 11:59:33 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon May 27 13:17:09 2024 +0200
@@ -360,6 +360,19 @@
}
+ /* decoration requests */
+
+ def force_decorations(channel: Channel, file: JFile): Unit = {
+ val model = state.value.models(file)
+ val rendering1 = rendering(model)
+ val (_, decos, model1) = model.publish_full(rendering1)
+ if (pide_extensions) {
+ channel.write(rendering1.decoration_output(decos).json(file))
+ }
+ }
+
+
+
/* spell checker */
val spell_checker = new Spell_Checker_Variable