Changes

Summary

clarified module name;
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
clarified module name;

Changeset 64623:83f012ce2567 by wenzelm: clarified module name;
The file was added	`src/Tools/VSCode/src/vscode_resources.scala`
The file was modified	`src/Pure/build-jars` (diff)
The file was modified	`src/Tools/VSCode/src/server.scala` (diff)
The file was removed	`src/Tools/VSCode/src/uri_resources.scala`
Changeset 64622:529bbb8977c7 by wenzelm: more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
The file was added	`src/Pure/PIDE/rendering.scala`
The file was added	`src/Tools/VSCode/etc/options`
The file was added	`src/Tools/VSCode/src/vscode_rendering.scala`
The file was modified	`etc/components` (diff)
The file was modified	`src/Pure/build-jars` (diff)
The file was modified	`src/Tools/VSCode/src/document_model.scala` (diff)
The file was modified	`src/Tools/VSCode/src/server.scala` (diff)
The file was modified	`src/Tools/jEdit/src/jedit_rendering.scala` (diff)
Changeset 64621:7116f2634e32 by wenzelm: clarified module name;
The file was added	`src/Tools/jEdit/src/jedit_rendering.scala`
The file was modified	`src/Tools/jEdit/lib/Tools/jedit` (diff)
The file was modified	`src/Tools/jEdit/src/bibtex_jedit.scala` (diff)
The file was modified	`src/Tools/jEdit/src/completion_popup.scala` (diff)
The file was modified	`src/Tools/jEdit/src/document_view.scala` (diff)
The file was modified	`src/Tools/jEdit/src/fold_handling.scala` (diff)
The file was modified	`src/Tools/jEdit/src/graphview_dockable.scala` (diff)
The file was modified	`src/Tools/jEdit/src/jedit_lib.scala` (diff)
The file was modified	`src/Tools/jEdit/src/output_dockable.scala` (diff)
The file was modified	`src/Tools/jEdit/src/plugin.scala` (diff)
The file was modified	`src/Tools/jEdit/src/pretty_text_area.scala` (diff)
The file was modified	`src/Tools/jEdit/src/pretty_tooltip.scala` (diff)
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala` (diff)
The file was modified	`src/Tools/jEdit/src/spell_checker.scala` (diff)
The file was modified	`src/Tools/jEdit/src/text_structure.scala` (diff)
The file was modified	`src/Tools/jEdit/src/token_markup.scala` (diff)
The file was removed	`src/Tools/jEdit/src/rendering.scala`