# HG changeset patch # User wenzelm # Date 1414943265 -3600 # Node ID f0f623005324df1fbf3f20b93cffce452bfc543f # Parent c399ae4b836f677709a5efaec5cb57410cad0c54 added update_header tool; diff -r c399ae4b836f -r f0f623005324 NEWS --- a/NEWS Sun Nov 02 16:39:54 2014 +0100 +++ b/NEWS Sun Nov 02 16:47:45 2014 +0100 @@ -172,7 +172,8 @@ before the initial 'theory' command. Obsolete proof commands 'sect', 'subsect', 'subsubsect' have been discontinued. The Obsolete 'header' command is still retained for some time, but should be replaced by -'chapter', 'section' etc. Minor INCOMPATIBILITY. +'chapter', 'section' etc. (using "isabelle update_header"). Minor +INCOMPATIBILITY. * Official support for "tt" style variants, via \isatt{...} or \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or diff -r c399ae4b836f -r f0f623005324 lib/Tools/update_header --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/update_header Sun Nov 02 16:47:45 2014 +0100 @@ -0,0 +1,60 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: replace obsolete theory header command + + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: isabelle $PRG [FILES|DIRS...]" + echo + echo " Options are:" + echo " -s COMMAND alternative heading command (default 'section')" + echo + echo " Recursively find .thy files and replace obsolete theory header commands" + echo " by 'section' (default), or 'chapter', 'subsection', 'subsubsection'." + echo + echo " Old versions of files are preserved by appending \"~~\"." + echo + exit 1 +} + + +## process command line + +#options + +SECTION="section" + +while getopts "s:" OPT +do + case "$OPT" in + s) + SECTION="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + +[ "$#" -eq 0 -o "$1" = "-?" ] && usage + +SPECS="$@"; shift "$#" + + +## main + +find $SPECS -name \*.thy -print0 | \ + xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Header "$SECTION" diff -r c399ae4b836f -r f0f623005324 src/Pure/Tools/update_header.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/update_header.scala Sun Nov 02 16:47:45 2014 +0100 @@ -0,0 +1,40 @@ +/* Title: Pure/Tools/update_header.scala + Author: Makarius + +Replace theory header command. +*/ + +package isabelle + + +object Update_Header +{ + def update_header(section: String, path: Path) + { + val text0 = File.read(path) + val text1 = + (for (tok <- Outer_Syntax.empty.scan(text0).iterator) + yield { if (tok.source == "header") section else tok.source }).mkString + + if (text0 != text1) { + Output.writeln("changing " + path) + File.write_backup2(path, text1) + } + } + + + /* command line entry point */ + + def main(args: Array[String]) + { + Command_Line.tool0 { + args.toList match { + case section :: files => + if (!Set("chapter", "section", "subsection", "subsubsection").contains(section)) + error("Bad heading command: " + quote(section)) + files.foreach(file => update_header(section, Path.explode(file))) + case _ => error("Bad arguments:\n" + cat_lines(args)) + } + } + } +} diff -r c399ae4b836f -r f0f623005324 src/Pure/build-jars --- a/src/Pure/build-jars Sun Nov 02 16:39:54 2014 +0100 +++ b/src/Pure/build-jars Sun Nov 02 16:47:45 2014 +0100 @@ -96,6 +96,7 @@ Tools/simplifier_trace.scala Tools/task_statistics.scala Tools/update_cartouches.scala + Tools/update_header.scala Tools/update_semicolons.scala library.scala term.scala