1.1 --- a/src/Pure/General/symbol.scala	Sat Aug 16 15:57:05 2008 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Sat Aug 16 15:57:06 2008 +0200
     1.3 @@ -8,23 +8,72 @@
     1.4  package isabelle
     1.5  
     1.6  import java.util.regex.Pattern
     1.7 +import java.io.File
     1.8 +import scala.io.Source
     1.9 +import scala.collection.mutable.HashMap
    1.10  
    1.11  
    1.12  object Symbol {
    1.13  
    1.14 -  /* Regular expressions */
    1.15 +  /* Regexp utils */
    1.16  
    1.17    private def compile(s: String) =
    1.18      Pattern.compile(s, Pattern.COMMENTS | Pattern.DOTALL)
    1.19  
    1.20 +
    1.21 +  /* Symbol regexps */
    1.22 +
    1.23    private val symbol_src = """ \\ \\? < (?:
    1.24        \^? [A-Za-z][A-Za-z0-9_']* |
    1.25        \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >"""
    1.26  
    1.27    private val bad_symbol_src = "(?!" + symbol_src + ")" +
    1.28 -    """ \\ \\? < (?: (?! \p{Space} | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
    1.29 +    """ \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
    1.30  
    1.31    val symbol_pattern = compile(symbol_src)
    1.32    val bad_symbol_pattern = compile(bad_symbol_src)
    1.33    val pattern = compile(symbol_src + "|" + bad_symbol_src + "| .")
    1.34 +
    1.35 +
    1.36 +  /* Symbol interpretation tables */
    1.37 +
    1.38 +  private val empty_pattern = compile(""" ^\s* (?: \#.* )? $ """)
    1.39 +  private val blank_pattern = compile(""" \s+ """)
    1.40 +  private val key_pattern = compile(""" (.+): """)
    1.41 +
    1.42 +  class Interpretation extends HashMap[String, List[(String, String)]] {
    1.43 +
    1.44 +    class BadEntry(val line: String) extends Exception
    1.45 +
    1.46 +    def read_line(line: String) = {
    1.47 +      def err() = throw new BadEntry ("Bad symbol specification: " + line)
    1.48 +
    1.49 +      def read_pairs(props: List[String]): List[(String, String)] = {
    1.50 +        props match {
    1.51 +          case Nil => Nil
    1.52 +          case _ :: Nil => err()
    1.53 +          case key :: value :: rest => {
    1.54 +            val key_matcher = key_pattern.matcher(key)
    1.55 +            if (key_matcher.matches) { (key_matcher.group(1) -> value) :: read_pairs(rest) }
    1.56 +            else err ()
    1.57 +          }
    1.58 +        }
    1.59 +      }
    1.60 +
    1.61 +      if (!empty_pattern.matcher(line).matches) {
    1.62 +        blank_pattern.split(line).toList match {
    1.63 +          case Nil => err()
    1.64 +          case symbol :: props => this + (symbol -> read_pairs(props))
    1.65 +        }
    1.66 +      }
    1.67 +    }
    1.68 +
    1.69 +    for (base <- List(IsabelleSystem.ISABELLE_HOME, IsabelleSystem.ISABELLE_HOME_USER)) {
    1.70 +      val file = new File(base + File.separator + "etc" + File.separator + "symbols")
    1.71 +      if (file.canRead) {
    1.72 +        for (line <- Source.fromFile(file).getLines) read_line(line)
    1.73 +      }
    1.74 +    }
    1.75 +  }
    1.76 +
    1.77  }