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