src/Pure/Tools/check_keywords.scala
changeset 59891 9ce697050455
child 59895 a68a0fec288d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/check_keywords.scala	Wed Apr 01 15:41:08 2015 +0200
     1.3 @@ -0,0 +1,37 @@
     1.4 +/*  Title:      Pure/Tools/check_keywords.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Check theory sources for conflicts with proposed keywords.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Check_Keywords
    1.14 +{
    1.15 +  def conflicts(
    1.16 +    keywords: Keyword.Keywords,
    1.17 +    check: Set[String],
    1.18 +    input: CharSequence,
    1.19 +    start: Token.Pos): List[(Token, Position.T)] =
    1.20 +  {
    1.21 +    object Parser extends Parse.Parser
    1.22 +    {
    1.23 +      private val conflict =
    1.24 +        position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
    1.25 +      private val other = token("token", _ => true)
    1.26 +      private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
    1.27 +
    1.28 +      val result =
    1.29 +        parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
    1.30 +          case Success(res, _) => for (Some(x) <- res) yield x
    1.31 +          case bad => error(bad.toString)
    1.32 +        }
    1.33 +    }
    1.34 +    Parser.result
    1.35 +  }
    1.36 +
    1.37 +  def conflicts(
    1.38 +    keywords: Keyword.Keywords, check: Set[String], path: Path): List[(Token, Position.T)] =
    1.39 +    conflicts(keywords, check, File.read(path), Token.Pos.file(path.expand.implode))
    1.40 +}