src/Pure/General/symbol.scala
changeset 27918 85942d2036a0
parent 27905 070b4a6a9d58
child 27923 7ebe9d38743a
equal deleted inserted replaced
27917:a374f889ac5a 27918:85942d2036a0
     6 */
     6 */
     7 
     7 
     8 package isabelle
     8 package isabelle
     9 
     9 
    10 import java.util.regex.Pattern
    10 import java.util.regex.Pattern
       
    11 import java.io.File
       
    12 import scala.io.Source
       
    13 import scala.collection.mutable.HashMap
    11 
    14 
    12 
    15 
    13 object Symbol {
    16 object Symbol {
    14 
    17 
    15   /* Regular expressions */
    18   /* Regexp utils */
    16 
    19 
    17   private def compile(s: String) =
    20   private def compile(s: String) =
    18     Pattern.compile(s, Pattern.COMMENTS | Pattern.DOTALL)
    21     Pattern.compile(s, Pattern.COMMENTS | Pattern.DOTALL)
       
    22 
       
    23 
       
    24   /* Symbol regexps */
    19 
    25 
    20   private val symbol_src = """ \\ \\? < (?:
    26   private val symbol_src = """ \\ \\? < (?:
    21       \^? [A-Za-z][A-Za-z0-9_']* |
    27       \^? [A-Za-z][A-Za-z0-9_']* |
    22       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >"""
    28       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >"""
    23 
    29 
    24   private val bad_symbol_src = "(?!" + symbol_src + ")" +
    30   private val bad_symbol_src = "(?!" + symbol_src + ")" +
    25     """ \\ \\? < (?: (?! \p{Space} | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
    31     """ \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
    26 
    32 
    27   val symbol_pattern = compile(symbol_src)
    33   val symbol_pattern = compile(symbol_src)
    28   val bad_symbol_pattern = compile(bad_symbol_src)
    34   val bad_symbol_pattern = compile(bad_symbol_src)
    29   val pattern = compile(symbol_src + "|" + bad_symbol_src + "| .")
    35   val pattern = compile(symbol_src + "|" + bad_symbol_src + "| .")
       
    36 
       
    37 
       
    38   /* Symbol interpretation tables */
       
    39 
       
    40   private val empty_pattern = compile(""" ^\s* (?: \#.* )? $ """)
       
    41   private val blank_pattern = compile(""" \s+ """)
       
    42   private val key_pattern = compile(""" (.+): """)
       
    43 
       
    44   class Interpretation extends HashMap[String, List[(String, String)]] {
       
    45 
       
    46     class BadEntry(val line: String) extends Exception
       
    47 
       
    48     def read_line(line: String) = {
       
    49       def err() = throw new BadEntry ("Bad symbol specification: " + line)
       
    50 
       
    51       def read_pairs(props: List[String]): List[(String, String)] = {
       
    52         props match {
       
    53           case Nil => Nil
       
    54           case _ :: Nil => err()
       
    55           case key :: value :: rest => {
       
    56             val key_matcher = key_pattern.matcher(key)
       
    57             if (key_matcher.matches) { (key_matcher.group(1) -> value) :: read_pairs(rest) }
       
    58             else err ()
       
    59           }
       
    60         }
       
    61       }
       
    62 
       
    63       if (!empty_pattern.matcher(line).matches) {
       
    64         blank_pattern.split(line).toList match {
       
    65           case Nil => err()
       
    66           case symbol :: props => this + (symbol -> read_pairs(props))
       
    67         }
       
    68       }
       
    69     }
       
    70 
       
    71     for (base <- List(IsabelleSystem.ISABELLE_HOME, IsabelleSystem.ISABELLE_HOME_USER)) {
       
    72       val file = new File(base + File.separator + "etc" + File.separator + "symbols")
       
    73       if (file.canRead) {
       
    74         for (line <- Source.fromFile(file).getLines) read_line(line)
       
    75       }
       
    76     }
       
    77   }
       
    78 
    30 }
    79 }