| author | wenzelm | 
| Sat, 30 Oct 2010 16:33:58 +0200 | |
| changeset 40291 | 012ed4426fda | 
| parent 35022 | c844b93dd147 | 
| child 52439 | 4cf3f6153eb8 | 
| permissions | -rwxr-xr-x | 
| 24875 | 1 | #!/usr/bin/env bash | 
| 2 | # | |
| 3 | # Author: Makarius | |
| 4 | # | |
| 5 | # DESCRIPTION: generate outer syntax keyword files from session logs | |
| 6 | ||
| 7 | ||
| 8 | ## diagnostics | |
| 9 | ||
| 10 | PRG="$(basename "$0")" | |
| 11 | ||
| 12 | function usage() | |
| 13 | {
 | |
| 14 | echo | |
| 28650 | 15 | echo "Usage: isabelle $PRG [OPTIONS] [LOGS ...]" | 
| 24875 | 16 | echo | 
| 17 | echo " Options are:" | |
| 18 | echo " -k NAME specific name of keywords collection (default: empty)" | |
| 19 | echo | |
| 20 | echo " Generate outer syntax keyword files from (compressed) session LOGS." | |
| 33684 | 21 | echo " Targets Emacs Proof General." | 
| 24875 | 22 | echo | 
| 23 | exit 1 | |
| 24 | } | |
| 25 | ||
| 26 | ||
| 27 | ## process command line | |
| 28 | ||
| 29 | # options | |
| 30 | ||
| 31 | KEYWORDS_NAME="" | |
| 32 | ||
| 33684 | 33 | while getopts "k:" OPT | 
| 24875 | 34 | do | 
| 35 | case "$OPT" in | |
| 36 | k) | |
| 37 | KEYWORDS_NAME="$OPTARG" | |
| 38 | ;; | |
| 39 | \?) | |
| 40 | usage | |
| 41 | ;; | |
| 42 | esac | |
| 43 | done | |
| 44 | ||
| 45 | shift $(($OPTIND - 1)) | |
| 46 | ||
| 47 | ||
| 48 | ## main | |
| 49 | ||
| 50 | SESSIONS="" | |
| 33684 | 51 | for LOG in "$@" | 
| 24875 | 52 | do | 
| 53 | NAME="$(basename "$LOG" .gz)" | |
| 24885 | 54 | if [ -z "$SESSIONS" ]; then | 
| 55 | SESSIONS="$NAME" | |
| 56 | else | |
| 57 | SESSIONS="$SESSIONS + $NAME" | |
| 24875 | 58 | fi | 
| 59 | done | |
| 60 | ||
| 33684 | 61 | for LOG in "$@" | 
| 24875 | 62 | do | 
| 63 |   if [ "${LOG%.gz}" = "$LOG" ]; then
 | |
| 64 | cat "$LOG" | |
| 65 | else | |
| 66 | gzip -dc "$LOG" | |
| 67 | fi | |
| 68 | echo | |
| 35022 
c844b93dd147
modernized perl scripts: prefer standalone executables;
 wenzelm parents: 
33684diff
changeset | 69 | done | "$ISABELLE_HOME/lib/scripts/keywords" "$KEYWORDS_NAME" "$SESSIONS" |