src/Pure/Tools/check_keywords.scala
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 65827 3bba3856b56c
child 67880 e59220a075de
permissions -rw-r--r--
tuned signature;
     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 check_keywords(
    35     progress: Progress,
    36     keywords: Keyword.Keywords,
    37     check: Set[String],
    38     paths: List[Path])
    39   {
    40     val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
    41 
    42     val bad =
    43       Par_List.map((arg: (String, Token.Pos)) => {
    44         if (progress.stopped) throw Exn.Interrupt()
    45         conflicts(keywords, check, arg._1, arg._2)
    46       }, parallel_args).flatten
    47 
    48     for ((tok, pos) <- bad) {
    49       progress.echo_warning(
    50         "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
    51     }
    52   }
    53 }