Changes

Summary

merged
tuned signature;
proper treatment of empty result;
clarified modules;
tuned signature;
provide spell-checker menu via completion commands;
added commands for spell-checker dictionary;
tuned signature;

Changeset 66144:8f1cbb77a70a by wenzelm: merged
Changeset 66143:51f74025a3e3 by wenzelm: tuned signature;
The file was modified	`src/Tools/VSCode/src/vscode_rendering.scala` (diff)
The file was modified	`src/Tools/VSCode/src/vscode_spell_checker.scala` (diff)
Changeset 66142:90629b166203 by wenzelm: proper treatment of empty result;
The file was modified	`src/Tools/VSCode/src/vscode_rendering.scala` (diff)
Changeset 66141:81c8bb1d33b9 by wenzelm: clarified modules;
The file was added	`src/Tools/VSCode/src/vscode_spell_checker.scala`
The file was modified	`src/Pure/build-jars` (diff)
The file was modified	`src/Tools/VSCode/src/vscode_rendering.scala` (diff)
Changeset 66140:cdb6c10122b6 by wenzelm: tuned signature;
The file was modified	`src/Tools/VSCode/src/protocol.scala` (diff)
The file was modified	`src/Tools/VSCode/src/vscode_rendering.scala` (diff)
Changeset 66139:6a8f8be2741c by wenzelm: provide spell-checker menu via completion commands;
The file was modified	`src/Tools/VSCode/src/protocol.scala` (diff)
The file was modified	`src/Tools/VSCode/src/vscode_rendering.scala` (diff)
Changeset 66138:f7ef4c50b747 by wenzelm: added commands for spell-checker dictionary;
The file was modified	`src/Tools/VSCode/extension/package.json` (diff)
The file was modified	`src/Tools/VSCode/extension/src/extension.ts` (diff)
The file was modified	`src/Tools/VSCode/extension/src/protocol.ts` (diff)
The file was modified	`src/Tools/VSCode/src/protocol.scala` (diff)
The file was modified	`src/Tools/VSCode/src/server.scala` (diff)
The file was modified	`src/Tools/VSCode/src/vscode_resources.scala` (diff)
Changeset 66137:d2923067b376 by wenzelm: tuned signature;
The file was modified	`src/Pure/Tools/spell_checker.scala` (diff)
The file was modified	`src/Tools/jEdit/src/jedit_spell_checker.scala` (diff)