# HG changeset patch
# User wenzelm
# Date 1699628632 -3600
# Node ID 7774e1372476fe4f8c3ccb853cce82eb69e4ee1d
# Parent  5e6b195eee83a38e3a8962aa27c13e411aadcca1
clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";

diff -r 5e6b195eee83 -r 7774e1372476 etc/settings
--- a/etc/settings	Thu Nov 09 15:11:52 2023 +0000
+++ b/etc/settings	Fri Nov 10 16:03:52 2023 +0100
@@ -141,7 +141,7 @@
 ### Symbol rendering
 ###
 
-ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
+ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols?"
 
 
 ###
diff -r 5e6b195eee83 -r 7774e1372476 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Nov 09 15:11:52 2023 +0000
+++ b/src/Pure/General/path.scala	Fri Nov 10 16:03:52 2023 +0100
@@ -129,6 +129,23 @@
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)
 
+  def split_permissive(str: String): List[(Path, Boolean)] =
+    space_explode(':', str).flatMap(
+      {
+        case "" | "?" => None
+        case s =>
+          Library.try_unsuffix("?", s) match {
+            case None => Some(explode(s) -> false)
+            case Some(p) => Some(explode(p) -> true)
+          }
+      })
+
+  def split_permissive_files(str: String): List[Path] =
+    for {
+      (path, permissive) <- split_permissive(str)
+      if !permissive || path.is_file
+    } yield path
+
 
   /* encode */
 
diff -r 5e6b195eee83 -r 7774e1372476 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Nov 09 15:11:52 2023 +0000
+++ b/src/Pure/General/symbol.scala	Fri Nov 10 16:03:52 2023 +0100
@@ -351,15 +351,12 @@
       code.map(c => new String(Character.toChars(c)))
   }
 
-  lazy val symbols: Symbols = Symbols.load()
+  lazy val symbols: Symbols =
+    Symbols.make(cat_lines(Symbols.files().map(File.read)))
 
   object Symbols {
-    def load(static: Boolean = false): Symbols = {
-      val paths =
-        if (static) List(Path.explode("~~/etc/symbols"))
-        else Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS"))
-      make(cat_lines(for (path <- paths if path.is_file) yield File.read(path)))
-    }
+    def files(): List[Path] =
+      Path.split_permissive_files(Isabelle_System.getenv("ISABELLE_SYMBOLS"))
 
     def make(symbols_spec: String): Symbols = {
       val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
diff -r 5e6b195eee83 -r 7774e1372476 src/Tools/VSCode/src/component_vscodium.scala
--- a/src/Tools/VSCode/src/component_vscodium.scala	Thu Nov 09 15:11:52 2023 +0000
+++ b/src/Tools/VSCode/src/component_vscodium.scala	Fri Nov 10 16:03:52 2023 +0100
@@ -26,8 +26,10 @@
 
   /* Isabelle symbols (static subset only) */
 
+  lazy val symbols: Symbol.Symbols =
+    Symbol.Symbols.make(File.read(Path.explode("~~/etc/symbols")))
+
   def make_symbols(): File.Content = {
-    val symbols = Symbol.Symbols.load(static = true)
     val symbols_js =
       JSON.Format.pretty_print(
         for (entry <- symbols.entries) yield
@@ -41,7 +43,6 @@
   }
 
   def make_isabelle_encoding(header: String): File.Content = {
-    val symbols = Symbol.Symbols.load(static = true)
     val symbols_js =
       JSON.Format.pretty_print(
         for (entry <- symbols.entries; code <- entry.code)