src/Pure/Tools/check_keywords.scala
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 65827 3bba3856b56c
child 67880 e59220a075de
permissions -rw-r--r--
tuned signature;
wenzelm@59891
     1
/*  Title:      Pure/Tools/check_keywords.scala
wenzelm@59891
     2
    Author:     Makarius
wenzelm@59891
     3
wenzelm@59891
     4
Check theory sources for conflicts with proposed keywords.
wenzelm@59891
     5
*/
wenzelm@59891
     6
wenzelm@59891
     7
package isabelle
wenzelm@59891
     8
wenzelm@59891
     9
wenzelm@59891
    10
object Check_Keywords
wenzelm@59891
    11
{
wenzelm@59891
    12
  def conflicts(
wenzelm@59891
    13
    keywords: Keyword.Keywords,
wenzelm@59891
    14
    check: Set[String],
wenzelm@59891
    15
    input: CharSequence,
wenzelm@59891
    16
    start: Token.Pos): List[(Token, Position.T)] =
wenzelm@59891
    17
  {
wenzelm@59891
    18
    object Parser extends Parse.Parser
wenzelm@59891
    19
    {
wenzelm@59891
    20
      private val conflict =
wenzelm@59891
    21
        position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
wenzelm@59891
    22
      private val other = token("token", _ => true)
wenzelm@59891
    23
      private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
wenzelm@59891
    24
wenzelm@59891
    25
      val result =
wenzelm@59891
    26
        parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
wenzelm@59891
    27
          case Success(res, _) => for (Some(x) <- res) yield x
wenzelm@59891
    28
          case bad => error(bad.toString)
wenzelm@59891
    29
        }
wenzelm@59891
    30
    }
wenzelm@59891
    31
    Parser.result
wenzelm@59891
    32
  }
wenzelm@59891
    33
wenzelm@59895
    34
  def check_keywords(
wenzelm@61276
    35
    progress: Progress,
wenzelm@59895
    36
    keywords: Keyword.Keywords,
wenzelm@59895
    37
    check: Set[String],
wenzelm@59895
    38
    paths: List[Path])
wenzelm@59895
    39
  {
wenzelm@59895
    40
    val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
wenzelm@59895
    41
wenzelm@59895
    42
    val bad =
wenzelm@59895
    43
      Par_List.map((arg: (String, Token.Pos)) => {
wenzelm@59895
    44
        if (progress.stopped) throw Exn.Interrupt()
wenzelm@59895
    45
        conflicts(keywords, check, arg._1, arg._2)
wenzelm@59895
    46
      }, parallel_args).flatten
wenzelm@59895
    47
wenzelm@59895
    48
    for ((tok, pos) <- bad) {
wenzelm@65827
    49
      progress.echo_warning(
wenzelm@65827
    50
        "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
wenzelm@59895
    51
    }
wenzelm@59895
    52
  }
wenzelm@59891
    53
}