src/Pure/Tools/build.scala
changeset 59891 9ce697050455
parent 59811 6b0d9e8ac227
child 59892 2a616319c171
     1.1 --- a/src/Pure/Tools/build.scala	Wed Apr 01 13:32:32 2015 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 01 15:41:08 2015 +0200
     1.3 @@ -427,8 +427,13 @@
     1.4      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
     1.5    }
     1.6  
     1.7 -  def dependencies(progress: Progress, inlined_files: Boolean,
     1.8 -      verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
     1.9 +  def dependencies(
    1.10 +      progress: Progress = Ignore_Progress,
    1.11 +      inlined_files: Boolean = false,
    1.12 +      verbose: Boolean = false,
    1.13 +      list_files: Boolean = false,
    1.14 +      check_keywords: Set[String] = Set.empty,
    1.15 +      tree: Session_Tree): Deps =
    1.16      Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
    1.17        { case (deps, (name, info)) =>
    1.18            if (progress.stopped) throw Exn.Interrupt()
    1.19 @@ -484,16 +489,28 @@
    1.20              val keywords = thy_deps.keywords
    1.21              val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
    1.22  
    1.23 +            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    1.24              val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
    1.25  
    1.26              val all_files =
    1.27 -              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
    1.28 +              (theory_files ::: loaded_files :::
    1.29                  info.files.map(file => info.dir + file) :::
    1.30                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    1.31  
    1.32              if (list_files)
    1.33                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    1.34  
    1.35 +            if (check_keywords.nonEmpty) {
    1.36 +              for {
    1.37 +                path <- theory_files
    1.38 +                (tok, pos) <- Check_Keywords.conflicts(syntax.keywords, check_keywords, path)
    1.39 +              } {
    1.40 +                progress.echo(Output.warning_text(
    1.41 +                  "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
    1.42 +                    Position.here(pos)))
    1.43 +              }
    1.44 +            }
    1.45 +
    1.46              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    1.47  
    1.48              val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
    1.49 @@ -517,7 +534,7 @@
    1.50      sessions: List[String]): Deps =
    1.51    {
    1.52      val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
    1.53 -    dependencies(Ignore_Progress, inlined_files, false, false, tree)
    1.54 +    dependencies(inlined_files = inlined_files, tree = tree)
    1.55    }
    1.56  
    1.57    def session_content(
    1.58 @@ -737,6 +754,7 @@
    1.59      session_groups: List[String] = Nil,
    1.60      max_jobs: Int = 1,
    1.61      list_files: Boolean = false,
    1.62 +    check_keywords: Set[String] = Set.empty,
    1.63      no_build: Boolean = false,
    1.64      system_mode: Boolean = false,
    1.65      verbose: Boolean = false,
    1.66 @@ -748,7 +766,7 @@
    1.67      val (selected, selected_tree) =
    1.68        full_tree.selection(requirements, all_sessions, session_groups, sessions)
    1.69  
    1.70 -    val deps = dependencies(progress, true, verbose, list_files, selected_tree)
    1.71 +    val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
    1.72  
    1.73      def make_stamp(name: String): String =
    1.74        sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
    1.75 @@ -988,6 +1006,7 @@
    1.76      session_groups: List[String] = Nil,
    1.77      max_jobs: Int = 1,
    1.78      list_files: Boolean = false,
    1.79 +    check_keywords: Set[String] = Set.empty,
    1.80      no_build: Boolean = false,
    1.81      system_mode: Boolean = false,
    1.82      verbose: Boolean = false,
    1.83 @@ -996,7 +1015,7 @@
    1.84      val results =
    1.85        build_results(options, progress, requirements, all_sessions,
    1.86          build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
    1.87 -        list_files, no_build, system_mode, verbose, sessions)
    1.88 +        list_files, check_keywords, no_build, system_mode, verbose, sessions)
    1.89  
    1.90      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
    1.91      if (rc != 0 && (verbose || !no_build)) {
    1.92 @@ -1024,13 +1043,15 @@
    1.93            Properties.Value.Boolean(no_build) ::
    1.94            Properties.Value.Boolean(system_mode) ::
    1.95            Properties.Value.Boolean(verbose) ::
    1.96 -          Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
    1.97 +          Command_Line.Chunks(
    1.98 +              dirs, select_dirs, session_groups, check_keywords, build_options, sessions) =>
    1.99              val options = (Options.init() /: build_options)(_ + _)
   1.100              val progress = new Console_Progress(verbose)
   1.101              progress.interrupt_handler {
   1.102                build(options, progress, requirements, all_sessions, build_heap, clean_build,
   1.103                  dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
   1.104 -                max_jobs, list_files, no_build, system_mode, verbose, sessions)
   1.105 +                max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
   1.106 +                verbose, sessions)
   1.107              }
   1.108          case _ => error("Bad arguments:\n" + cat_lines(args))
   1.109        }