# HG changeset patch
# User wenzelm
# Date 1675245269 -3600
# Node ID 547d140f07803326cb76d41ad37f2c14c878882e
# Parent  646e36bf24aeca5658b82dea3f38215b35f7648b
more uniform use of Symbol.output, even in situations where its Symbol.encode is usually redundant;

diff -r 646e36bf24ae -r 547d140f0780 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Feb 01 09:14:40 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Wed Feb 01 10:54:29 2023 +0100
@@ -647,8 +647,7 @@
           if (!node_name.is_theory) error("Not a theory file: " + path)
 
           progress.expose_interrupt()
-          val text0 = File.read(path)
-          val text = if (unicode_symbols) Symbol.decode(text0) else text0
+          val text = Symbol.output(unicode_symbols, File.read(path))
           val node_header = resources.check_thy(node_name, Scan.char_reader(text))
           new Resources.Theory(node_name, node_header, text, true)
         }
diff -r 646e36bf24ae -r 547d140f0780 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Wed Feb 01 09:14:40 2023 +0100
+++ b/src/Pure/Thy/export.scala	Wed Feb 01 10:54:29 2023 +0100
@@ -447,10 +447,7 @@
         for {
           name <- theory_context.files0(permissive = true).headOption
           file <- get_source_file(name)
-        } yield {
-          val text0 = file.bytes.text
-          if (unicode_symbols) Symbol.decode(text0) else text0
-        }
+        } yield Symbol.output(unicode_symbols, file.bytes.text)
       }
 
       snapshot_source orElse db_source getOrElse ""