# HG changeset patch
# User wenzelm
# Date 1754487137 -7200
# Node ID e5fa061b95706cdd17def6f450b065fd74a0f400
# Parent  7185406956cd1d513310c251d88db0e4b5b80734
more accurate treatment unicode_symbols (for main theory file);

diff -r 7185406956cd -r e5fa061b9570 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Aug 06 14:06:16 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Aug 06 15:32:17 2025 +0200
@@ -130,6 +130,11 @@
       override def session_options: Options = options
       override def resources: Resources = Resources.bootstrap
     }
+
+
+  /* read_theory cache */
+
+  sealed case class Read_Theory_Key(name: String, unicode_symbols: Boolean)
 }
 
 
@@ -157,22 +162,24 @@
       store, resources.session_background, document_snapshot = document_snapshot)
   }
 
-  private val read_theory_cache = new WeakHashMap[String, WeakReference[Document.Snapshot]]
+  private val read_theory_cache =
+    new WeakHashMap[Session.Read_Theory_Key, WeakReference[Document.Snapshot]]
 
-  def read_theory(name: String): Document.Snapshot =
+  def read_theory(name: String, unicode_symbols: Boolean = false): Document.Snapshot =
     read_theory_cache.synchronized {
-      Option(read_theory_cache.get(name)).map(_.get) match {
+      val key = Session.Read_Theory_Key(name, unicode_symbols)
+      Option(read_theory_cache.get(key)).map(_.get) match {
         case Some(snapshot: Document.Snapshot) => snapshot
         case _ =>
           val maybe_snapshot =
             using(open_session_context()) { session_context =>
               Build.read_theory(session_context.theory(name),
-                unicode_symbols = true,
+                unicode_symbols = unicode_symbols,
                 migrate_file = (a: String) => session.resources.append_path("", Path.explode(a)))
             }
           maybe_snapshot.map(_.snippet_commands) match {
             case Some(List(_)) =>
-              read_theory_cache.put(name, new WeakReference(maybe_snapshot.get))
+              read_theory_cache.put(key, new WeakReference(maybe_snapshot.get))
               maybe_snapshot.get
             case _ => error("Failed to load theory " + quote(name) + " from session database")
           }
diff -r 7185406956cd -r e5fa061b9570 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 06 14:06:16 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 06 15:32:17 2025 +0200
@@ -160,13 +160,16 @@
     require(node_name.is_theory)
     val theory = node_name.theory
 
-    Exn.capture(session.read_theory(theory)) match {
+    val node_source = node.source
+    val unicode_symbols = Symbol.decode(node_source) == node_source
+
+    Exn.capture(session.read_theory(theory, unicode_symbols = unicode_symbols)) match {
       case Exn.Res(snapshot) =>
         val command = snapshot.snippet_commands.head
         val node_commands =
           if (node.is_empty) Linear_Set.empty
           else {
-            val thy_changed = if (node.source == command.source) Nil else List(node_name.node)
+            val thy_changed = if (node_source == command.source) Nil else List(node_name.node)
             val blobs_changed =
               List.from(
                 for {