# HG changeset patch
# User wenzelm
# Date 1232471077 -3600
# Node ID f3f529b5d8fba833463d261635420dd44418add3
# Parent  ba144750086d4424c371b795c681adcb51dcb67b
more general init of Symbol.Interpretation, independent of IsabelleSystem instance;

diff -r ba144750086d -r f3f529b5d8fb src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Jan 19 23:40:29 2009 +0100
+++ b/src/Pure/General/symbol.scala	Tue Jan 20 18:04:37 2009 +0100
@@ -78,9 +78,9 @@
 
   /** Symbol interpretation **/
 
-  class Interpretation(isabelle_system: IsabelleSystem) {
-
-    private var symbols = new HashMap[String, HashMap[String, String]]
+  class Interpretation(symbol_decls: Iterator[String])
+  {
+    private val symbols = new HashMap[String, HashMap[String, String]]
     private var decoder: Recoder = null
     private var encoder: Recoder = null
 
@@ -94,10 +94,11 @@
     private val blank_pattern = compile(""" \s+ """)
     private val key_pattern = compile(""" (.+): """)
 
-    private def read_line(line: String) = {
-      def err() = error("Bad symbol specification (line " + line + ")")
+    private def read_decl(decl: String) = {
+      def err() = error("Bad symbol declaration: " + decl)
 
-      def read_props(props: List[String], tab: HashMap[String, String]): Unit = {
+      def read_props(props: List[String], tab: HashMap[String, String])
+      {
         props match {
           case Nil => ()
           case _ :: Nil => err()
@@ -112,8 +113,8 @@
         }
       }
 
-      if (!empty_pattern.matcher(line).matches) {
-        blank_pattern.split(line).toList match {
+      if (!empty_pattern.matcher(decl).matches) {
+        blank_pattern.split(decl).toList match {
           case Nil => err()
           case symbol :: props => {
             val tab = new HashMap[String, String]
@@ -124,13 +125,6 @@
       }
     }
 
-    private def read_symbols(path: String) = {
-      val file = new File(isabelle_system.platform_path(path))
-      if (file.canRead) {
-        for (line <- Source.fromFile(file).getLines) read_line(line)
-      }
-    }
-
 
     /* init tables */
 
@@ -154,9 +148,7 @@
 
     /* constructor */
 
-    read_symbols("$ISABELLE_HOME/etc/symbols")
-    read_symbols("$ISABELLE_HOME_USER/etc/symbols")
+    symbol_decls.foreach(read_decl)
     init_recoders()
   }
-
 }