src/Pure/Tools/check_keywords.scala
author wenzelm
Wed Apr 01 15:41:08 2015 +0200 (2015-04-01)
changeset 59891 9ce697050455
child 59895 a68a0fec288d
permissions -rw-r--r--
added isabelle build option -k, for fast off-line checking of theory sources;
     1 /*  Title:      Pure/Tools/check_keywords.scala
     2     Author:     Makarius
     3 
     4 Check theory sources for conflicts with proposed keywords.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Check_Keywords
    11 {
    12   def conflicts(
    13     keywords: Keyword.Keywords,
    14     check: Set[String],
    15     input: CharSequence,
    16     start: Token.Pos): List[(Token, Position.T)] =
    17   {
    18     object Parser extends Parse.Parser
    19     {
    20       private val conflict =
    21         position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
    22       private val other = token("token", _ => true)
    23       private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
    24 
    25       val result =
    26         parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
    27           case Success(res, _) => for (Some(x) <- res) yield x
    28           case bad => error(bad.toString)
    29         }
    30     }
    31     Parser.result
    32   }
    33 
    34   def conflicts(
    35     keywords: Keyword.Keywords, check: Set[String], path: Path): List[(Token, Position.T)] =
    36     conflicts(keywords, check, File.read(path), Token.Pos.file(path.expand.implode))
    37 }