--- a/src/Pure/Tools/build.scala Wed Apr 01 13:32:32 2015 +0200
+++ b/src/Pure/Tools/build.scala Wed Apr 01 15:41:08 2015 +0200
@@ -427,8 +427,13 @@
def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
}
- def dependencies(progress: Progress, inlined_files: Boolean,
- verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
+ def dependencies(
+ progress: Progress = Ignore_Progress,
+ inlined_files: Boolean = false,
+ verbose: Boolean = false,
+ list_files: Boolean = false,
+ check_keywords: Set[String] = Set.empty,
+ tree: Session_Tree): Deps =
Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
if (progress.stopped) throw Exn.Interrupt()
@@ -484,16 +489,28 @@
val keywords = thy_deps.keywords
val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
+ val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
val all_files =
- (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
+ (theory_files ::: loaded_files :::
info.files.map(file => info.dir + file) :::
info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
if (list_files)
progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
+ if (check_keywords.nonEmpty) {
+ for {
+ path <- theory_files
+ (tok, pos) <- Check_Keywords.conflicts(syntax.keywords, check_keywords, path)
+ } {
+ progress.echo(Output.warning_text(
+ "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
+ Position.here(pos)))
+ }
+ }
+
val sources = all_files.map(p => (p, SHA1.digest(p.file)))
val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
@@ -517,7 +534,7 @@
sessions: List[String]): Deps =
{
val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
- dependencies(Ignore_Progress, inlined_files, false, false, tree)
+ dependencies(inlined_files = inlined_files, tree = tree)
}
def session_content(
@@ -737,6 +754,7 @@
session_groups: List[String] = Nil,
max_jobs: Int = 1,
list_files: Boolean = false,
+ check_keywords: Set[String] = Set.empty,
no_build: Boolean = false,
system_mode: Boolean = false,
verbose: Boolean = false,
@@ -748,7 +766,7 @@
val (selected, selected_tree) =
full_tree.selection(requirements, all_sessions, session_groups, sessions)
- val deps = dependencies(progress, true, verbose, list_files, selected_tree)
+ val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
def make_stamp(name: String): String =
sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
@@ -988,6 +1006,7 @@
session_groups: List[String] = Nil,
max_jobs: Int = 1,
list_files: Boolean = false,
+ check_keywords: Set[String] = Set.empty,
no_build: Boolean = false,
system_mode: Boolean = false,
verbose: Boolean = false,
@@ -996,7 +1015,7 @@
val results =
build_results(options, progress, requirements, all_sessions,
build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
- list_files, no_build, system_mode, verbose, sessions)
+ list_files, check_keywords, no_build, system_mode, verbose, sessions)
val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
if (rc != 0 && (verbose || !no_build)) {
@@ -1024,13 +1043,15 @@
Properties.Value.Boolean(no_build) ::
Properties.Value.Boolean(system_mode) ::
Properties.Value.Boolean(verbose) ::
- Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
+ Command_Line.Chunks(
+ dirs, select_dirs, session_groups, check_keywords, build_options, sessions) =>
val options = (Options.init() /: build_options)(_ + _)
val progress = new Console_Progress(verbose)
progress.interrupt_handler {
build(options, progress, requirements, all_sessions, build_heap, clean_build,
dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
- max_jobs, list_files, no_build, system_mode, verbose, sessions)
+ max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
+ verbose, sessions)
}
case _ => error("Bad arguments:\n" + cat_lines(args))
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/check_keywords.scala Wed Apr 01 15:41:08 2015 +0200
@@ -0,0 +1,37 @@
+/* Title: Pure/Tools/check_keywords.scala
+ Author: Makarius
+
+Check theory sources for conflicts with proposed keywords.
+*/
+
+package isabelle
+
+
+object Check_Keywords
+{
+ def conflicts(
+ keywords: Keyword.Keywords,
+ check: Set[String],
+ input: CharSequence,
+ start: Token.Pos): List[(Token, Position.T)] =
+ {
+ object Parser extends Parse.Parser
+ {
+ private val conflict =
+ position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
+ private val other = token("token", _ => true)
+ private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
+
+ val result =
+ parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
+ case Success(res, _) => for (Some(x) <- res) yield x
+ case bad => error(bad.toString)
+ }
+ }
+ Parser.result
+ }
+
+ def conflicts(
+ keywords: Keyword.Keywords, check: Set[String], path: Path): List[(Token, Position.T)] =
+ conflicts(keywords, check, File.read(path), Token.Pos.file(path.expand.implode))
+}