equal
deleted
inserted
replaced
36 # options |
36 # options |
37 |
37 |
38 CLEAN="" |
38 CLEAN="" |
39 NAME="document" |
39 NAME="document" |
40 OUTFORMAT=dvi |
40 OUTFORMAT=dvi |
41 TAGS="" |
41 declare -a TAGS=() |
42 |
42 |
43 while getopts "cn:o:t:" OPT |
43 while getopts "cn:o:t:" OPT |
44 do |
44 do |
45 case "$OPT" in |
45 case "$OPT" in |
46 c) |
46 c) |
51 ;; |
51 ;; |
52 o) |
52 o) |
53 OUTFORMAT="$OPTARG" |
53 OUTFORMAT="$OPTARG" |
54 ;; |
54 ;; |
55 t) |
55 t) |
56 TAGS="$OPTARG" |
56 ORIG_IFS="$IFS"; IFS=","; TAGS=($OPTARG); IFS="$ORIG_IFS" |
57 ;; |
57 ;; |
58 \?) |
58 \?) |
59 usage |
59 usage |
60 ;; |
60 ;; |
61 esac |
61 esac |
88 # tagged region markup |
88 # tagged region markup |
89 |
89 |
90 function prep_tags () |
90 function prep_tags () |
91 { |
91 { |
92 ( |
92 ( |
93 IFS="," |
93 for TAG in "${TAGS[@]}" |
94 for TAG in $TAGS |
|
95 do |
94 do |
96 case "$TAG" in |
95 case "$TAG" in |
97 /*) |
96 /*) |
98 echo "\\isafoldtag{${TAG:1}}" |
97 echo "\\isafoldtag{${TAG:1}}" |
99 ;; |
98 ;; |
100 -*) |
99 -*) |
101 echo "\\isadroptag{${TAG:1}}" |
100 echo "\\isadroptag{${TAG:1}}" |
102 ;; |
101 ;; |
103 +*) |
102 +*) |
104 echo "\\isakeeptag{${TAG:1}}" |
103 echo "\\isakeeptag{${TAG:1}}" |
105 ;; |
104 ;; |
106 *) |
105 *) |
107 echo "\\isakeeptag{${TAG}}" |
106 echo "\\isakeeptag{${TAG}}" |
108 ;; |
107 ;; |
109 esac |
108 esac |
110 done |
109 done |
111 ) > isabelletags.sty |
110 ) > isabelletags.sty |
112 } |
111 } |