src/Pure/Tools/check_keywords.scala

--- 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)
+        }
+      })
 }