# HG changeset patch # User wenzelm # Date 1726494576 -7200 # Node ID 5d562dd387aea03c00a4ff2797da5c05a2cd26dc # Parent 42ab8c52067e5b528a87c393a3256a8bbdbdd66f discontinued "isabelle build -k": superseded by admin-tool "isabelle check_keywords"; diff -r 42ab8c52067e -r 5d562dd387ae src/Doc/System/Sessions.thy --- 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>\-l\ lists the source files that contribute to a session. \<^medskip> - Option \<^verbatim>\-k\ specifies a newly proposed keyword for outer syntax. It is - possible to use option \<^verbatim>\-k\ 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>\-H\ augments the cluster hosts to be used in this build process. Each \<^verbatim>\-H\ option accepts multiple host or cluster names (separated by commas), which all share the same (optional) parameters or system options. diff -r 42ab8c52067e -r 5d562dd387ae src/Pure/Build/build.scala --- 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, diff -r 42ab8c52067e -r 5d562dd387ae src/Pure/Build/sessions.scala --- 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, diff -r 42ab8c52067e -r 5d562dd387ae src/Pure/System/isabelle_tool.scala --- 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, diff -r 42ab8c52067e -r 5d562dd387ae 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) + } + }) }