src/Pure/General/symbol.scala
changeset 78938 7774e1372476
parent 78599 1ce1abed5082
child 80437 2c07b9b2f9f4
--- 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* (?: \#.* )? $ """)