discontinued "isabelle build -k": superseded by admin-tool "isabelle check_keywords";

--- a/src/Doc/System/Sessions.thy	Mon Sep 16 15:39:35 2024 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Sep 16 15:49:36 2024 +0200
@@ -378,7 +378,6 @@
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs
                  (default: 1 for local build, 0 for build cluster)
-    -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- take existing session build databases
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -508,12 +507,6 @@
   Option \<^verbatim>\<open>-l\<close> lists the source files that contribute to a session.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax. It is
-  possible to use option \<^verbatim>\<open>-k\<close> repeatedly to check multiple keywords. The
-  theory sources are checked for conflicts wrt.\ this hypothetical change of
-  syntax, e.g.\ to reveal occurrences of identifiers that need to be quoted.
-
-  \<^medskip>
   Option \<^verbatim>\<open>-H\<close> augments the cluster hosts to be used in this build process.
   Each \<^verbatim>\<open>-H\<close> option accepts multiple host or cluster names (separated by
   commas), which all share the same (optional) parameters or system options.

--- a/src/Pure/Build/build.scala	Mon Sep 16 15:39:35 2024 +0200
+++ b/src/Pure/Build/build.scala	Mon Sep 16 15:49:36 2024 +0200
@@ -175,7 +175,6 @@
     numa_shuffling: Boolean = false,
     max_jobs: Option[Int] = None,
     list_files: Boolean = false,
-    check_keywords: Set[String] = Set.empty,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     soft_build: Boolean = false,
@@ -200,8 +199,7 @@
       val build_deps = {
         val deps0 =
           Sessions.deps(full_sessions.selection(selection), progress = progress,
-            inlined_files = true, list_files = list_files, check_keywords = check_keywords
-          ).check_errors
+            inlined_files = true, list_files = list_files).check_errors
 
         if (soft_build && !fresh_build) {
           val outdated =
@@ -336,7 +334,6 @@
       var fresh_build = false
       val session_groups = new mutable.ListBuffer[String]
       var max_jobs: Option[Int] = None
-      var check_keywords: Set[String] = Set.empty
       var list_files = false
       var no_build = false
       var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
@@ -400,7 +397,6 @@
         "f" -> (_ => fresh_build = true),
         "g:" -> (arg => session_groups += arg),
         "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
-        "k:" -> (arg => check_keywords = check_keywords + arg),
         "l" -> (_ => list_files = true),
         "n" -> (_ => no_build = true),
         "o:" -> (arg => options = options + arg),
@@ -439,7 +435,6 @@
             numa_shuffling = Host.numa_check(progress, numa_shuffling),
             max_jobs = max_jobs,
             list_files = list_files,
-            check_keywords = check_keywords,
             fresh_build = fresh_build,
             no_build = no_build,
             soft_build = soft_build,

--- a/src/Pure/Build/sessions.scala	Mon Sep 16 15:39:35 2024 +0200
+++ b/src/Pure/Build/sessions.scala	Mon Sep 16 15:49:36 2024 +0200
@@ -44,11 +44,10 @@
   def deps(sessions_structure: Structure,
     progress: Progress = new Progress,
     inlined_files: Boolean = false,
-    list_files: Boolean = false,
-    check_keywords: Set[String] = Set.empty
+    list_files: Boolean = false
   ): Deps = {
     Deps.load(sessions_structure, progress = progress, inlined_files = inlined_files,
-      list_files = list_files, check_keywords = check_keywords)
+      list_files = list_files)
   }
 
 
@@ -252,8 +251,7 @@
     def load(sessions_structure: Structure,
       progress: Progress = new Progress,
       inlined_files: Boolean = false,
-      list_files: Boolean = false,
-      check_keywords: Set[String] = Set.empty
+      list_files: Boolean = false
     ): Deps = {
       var cache_sources = Map.empty[JFile, SHA1.Digest]
       def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = {
@@ -292,8 +290,6 @@
 
               val dependencies = resources.session_dependencies(info)
 
-              val overall_syntax = dependencies.overall_syntax
-
               val proper_session_theories =
                 dependencies.theories.filter(name =>
                   sessions_structure.theory_qualifier(name) == session_name)
@@ -326,11 +322,6 @@
                 progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
               }
 
-              if (check_keywords.nonEmpty) {
-                Check_Keywords.check_keywords(
-                  progress, overall_syntax.keywords, check_keywords, theory_files)
-              }
-
               val session_graph_display: Graph_Display.Graph = {
                 def session_node(name: String): Graph_Display.Node =
                   Graph_Display.Node("[" + name + "]", "session." + name)
@@ -471,7 +462,7 @@
                   theory_load_commands = theory_load_commands,
                   known_theories = known_theories,
                   known_loaded_files = known_loaded_files,
-                  overall_syntax = overall_syntax,
+                  overall_syntax = dependencies.overall_syntax,
                   imported_sources = check_sources(imported_files),
                   session_sources = check_sources(session_files),
                   session_graph_display = session_graph_display,

--- a/src/Pure/System/isabelle_tool.scala	Mon Sep 16 15:39:35 2024 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Mon Sep 16 15:49:36 2024 +0200
@@ -168,6 +168,7 @@
   Build_Doc.isabelle_tool,
   Build_Log.isabelle_tool,
   Build_Status.isabelle_tool,
+  Check_Keywords.isabelle_tool,
   Check_Sources.isabelle_tool,
   Component_Bash_Process.isabelle_tool,
   Component_CSDP.isabelle_tool,

--- a/src/Pure/Tools/check_keywords.scala	Mon Sep 16 15:39:35 2024 +0200
+++ b/src/Pure/Tools/check_keywords.scala	Mon Sep 16 15:49:36 2024 +0200
@@ -8,45 +8,88 @@
 
 
 object Check_Keywords {
-  def conflicts(
-    keywords: Keyword.Keywords,
-    check: Set[String],
-    input: CharSequence,
-    start: Token.Pos
-  ): List[(Token, Position.T)] = {
-    object Parsers extends Parse.Parsers {
-      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: List[(Token, Position.T)] =
-        parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
-          case Success(res, _) => for (case Some(x) <- res) yield x
-          case bad => error(bad.toString)
-        }
-    }
-    Parsers.result
-  }
+  /* session theories for keyword conflicts */
 
   def check_keywords(
-    progress: Progress,
-    keywords: Keyword.Keywords,
+    options: Options,
     check: Set[String],
-    paths: List[Path]
+    dirs: List[Path] = Nil,
+    progress: Progress,
   ): Unit = {
-    val parallel_args =
-      paths.map(path => (File.read(path), Token.Pos.file(File.standard_path(path))))
+    val deps = Sessions.deps(Sessions.load_structure(options, dirs = dirs), progress = progress)
 
     val bad =
-      Par_List.map({ (arg: (String, Token.Pos)) =>
-        progress.expose_interrupt()
-        conflicts(keywords, check, arg._1, arg._2)
-      }, parallel_args).flatten
+      Par_List.maps[(Keyword.Keywords, String, Token.Pos), (Token, Position.T)](
+        { case (keywords, input, start) =>
+          progress.expose_interrupt()
+
+          object Parsers extends Parse.Parsers {
+            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: List[(Token, Position.T)] =
+              parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
+                case Success(res, _) => for (case Some(x) <- res) yield x
+                case bad => error(bad.toString)
+              }
+          }
+          Parsers.result
+        },
+        List.from(
+          for {
+            session <- deps.sessions_structure.imports_topological_order.iterator
+            base = deps(session)
+            node_name <- base.proper_session_theories
+          } yield {
+            val path = node_name.path
+            val input = File.read(path)
+            val start = Token.Pos.file(File.standard_path(path))
+            (base.overall_syntax.keywords, input, start)
+          })
+      )
 
     for ((tok, pos) <- bad) {
       progress.echo_warning(
         "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
     }
   }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("check_keywords", "check theory sources for conflicts with proposed keywords",
+      Scala_Project.here,
+      { args =>
+        var dirs: List[Path] = Nil
+        var options = Options.init()
+        var verbose = false
+
+        val getopts = Getopts("""
+Usage: isabelle check_keywords [OPTIONS] KEYWORDS
+
+  Options are:
+    -d DIR       include session directory
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -v           verbose
+
+  Check theory sources from all session directories for conflicts with
+  newly proposed keywords (outer syntax). This reveals occurrences of
+  identifiers that would have to be quoted.
+""",
+        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+        "o:" -> (arg => options = options + arg),
+        "v" -> (_ => verbose = true))
+
+        val keywords = getopts(args)
+        if (keywords.isEmpty) getopts.usage()
+
+        val progress = new Console_Progress(verbose = verbose)
+
+        progress.interrupt_handler {
+          check_keywords(options, keywords.toSet, dirs = dirs, progress = progress)
+        }
+      })
 }