# HG changeset patch
# User wenzelm
# Date 1665747325 -7200
# Node ID 072e6c0a237358643f8fc9a7fbd83025868b02a5
# Parent  2d4ff8c166d299d3b16e63fe6084567964584d3b
proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with symbols like \<^here>;

diff -r 2d4ff8c166d2 -r 072e6c0a2373 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala	Fri Oct 14 13:35:25 2022 +0200
@@ -36,7 +36,7 @@
     def text_range: Text.Range = doc.text_range
     def text: String = doc.text
 
-    lazy val bytes: Bytes = Bytes(text)
+    lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
     lazy val bibtex_entries: List[Text.Info[String]] =
       try { Bibtex.entries(text) }