1/*  Title:      Pure/Tools/check_keywords.scala
2    Author:     Makarius
3
4Check theory sources for conflicts with proposed keywords.
5*/
6
7package isabelle
8
9
10object 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        progress.expose_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}
54