# HG changeset patch # User wenzelm # Date 1427895668 -7200 # Node ID 9ce6970504552e153ad0c9367e94ac4ca517abd8 # Parent 01aff5aa081d6ba6e660ca2c281477efc7c92e47 added isabelle build option -k, for fast off-line checking of theory sources; diff -r 01aff5aa081d -r 9ce697050455 NEWS --- a/NEWS Wed Apr 01 13:32:32 2015 +0200 +++ b/NEWS Wed Apr 01 15:41:08 2015 +0200 @@ -396,6 +396,8 @@ * The Isabelle tool "update_cartouches" changes theory files to use cartouches instead of old-style {* verbatim *} or `alt_string` tokens. +* The Isabelle tool "build" provides new option -k. + New in Isabelle2014 (August 2014) diff -r 01aff5aa081d -r 9ce697050455 lib/Tools/build --- a/lib/Tools/build Wed Apr 01 13:32:32 2015 +0200 +++ b/lib/Tools/build Wed Apr 01 15:41:08 2015 +0200 @@ -34,6 +34,7 @@ echo " -d DIR include session directory" echo " -g NAME select session group NAME" echo " -j INT maximum number of parallel jobs (default 1)" + echo " -k KEYWORD check theory sources for conflicts with proposed keywords" echo " -l list session source files" echo " -n no build -- test dependencies only" echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)" @@ -68,13 +69,14 @@ declare -a INCLUDE_DIRS=() declare -a SESSION_GROUPS=() MAX_JOBS=1 +declare -a CHECK_KEYWORDS=() LIST_FILES=false NO_BUILD=false eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" SYSTEM_MODE=false VERBOSE=false -while getopts "D:Rabcd:g:j:lno:sv" OPT +while getopts "D:Rabcd:g:j:k:lno:sv" OPT do case "$OPT" in D) @@ -102,6 +104,9 @@ check_number "$OPTARG" MAX_JOBS="$OPTARG" ;; + k) + CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG" + ;; l) LIST_FILES="true" ;; @@ -145,7 +150,8 @@ "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \ "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \ - "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" + "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \ + "${BUILD_OPTIONS[@]}" $'\n' "$@" RC="$?" if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then diff -r 01aff5aa081d -r 9ce697050455 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Wed Apr 01 13:32:32 2015 +0200 +++ b/src/Doc/System/Sessions.thy Wed Apr 01 15:41:08 2015 +0200 @@ -284,6 +284,7 @@ -d DIR include session directory -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) + -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files -n no build -- test dependencies only -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) @@ -369,7 +370,12 @@ \medskip Option @{verbatim "-v"} increases the general level of verbosity. Option @{verbatim "-l"} lists the source files that contribute to a session. -\ + + \medskip Option @{verbatim "-k"} specifies a newly proposed keyword for + outer syntax (multiple uses allowed). 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.\ + subsubsection \Examples\ diff -r 01aff5aa081d -r 9ce697050455 src/Pure/PIDE/batch_session.scala --- a/src/Pure/PIDE/batch_session.scala Wed Apr 01 13:32:32 2015 +0200 +++ b/src/Pure/PIDE/batch_session.scala Wed Apr 01 15:41:08 2015 +0200 @@ -29,7 +29,7 @@ dirs = dirs, sessions = List(parent_session)) != 0) new RuntimeException - val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree) + val deps = Build.dependencies(verbose = verbose, tree = session_tree) val resources = { val content = deps(parent_session) diff -r 01aff5aa081d -r 9ce697050455 src/Pure/Tools/build.scala --- 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)) } diff -r 01aff5aa081d -r 9ce697050455 src/Pure/Tools/check_keywords.scala --- /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)) +} diff -r 01aff5aa081d -r 9ce697050455 src/Pure/build-jars --- a/src/Pure/build-jars Wed Apr 01 13:32:32 2015 +0200 +++ b/src/Pure/build-jars Wed Apr 01 15:41:08 2015 +0200 @@ -92,6 +92,7 @@ Tools/build.scala Tools/build_console.scala Tools/build_doc.scala + Tools/check_keywords.scala Tools/check_source.scala Tools/doc.scala Tools/main.scala