diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/change-header | 55 | ||||
| -rwxr-xr-x | dev/tools/univdot | 49 |
2 files changed, 55 insertions, 49 deletions
diff --git a/dev/tools/change-header b/dev/tools/change-header new file mode 100755 index 00000000..61cc8666 --- /dev/null +++ b/dev/tools/change-header @@ -0,0 +1,55 @@ +#!/bin/sh + +#This script changes the header of .ml* files + +if [ ! $# = 2 ]; then + echo Usage: change-header old-header-file new-header-file + exit 1 +fi + +oldheader=$1 +newheader=$2 + +if [ ! -f $oldheader ]; then echo Cannot read file $oldheader; exit 1; fi +if [ ! -f $newheader ]; then echo Cannot read file $newheader; exit 1; fi + +n=`wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g"` +nsucc=`expr $n + 1` + +linea='(* -*- coding:utf-8 -*- *)' +lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' + +modified=0 +kept=0 + +for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do + headline=`head -n 1 $i` + if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then + # Has emacs header + head -n +$nsucc $i | tail -n $n > $i.head.tmp$$ + hasheadline=1 + nnext=`expr $nsucc + 1` + else + head -n +$n $i > $i.head.tmp$$ + hasheadline=0 + nnext=$nsucc + fi + if diff -a -q $oldheader $i.head.tmp$$ > /dev/null; then + echo "$i: header changed" + if [ $hasheadline = 1 ]; then + echo $headline > $i.tmp$$ + else + touch $i.tmp$$ + fi + cat $newheader >> $i.tmp$$ + tail -n +$nnext $i >> $i.tmp$$ + mv $i.tmp$$ $i + modified=`expr $modified + 1` + else + kept=`expr $kept + 1` + fi + rm $i.head.tmp$$ +done + +echo $modified files updated +echo $kept files unchanged diff --git a/dev/tools/univdot b/dev/tools/univdot deleted file mode 100755 index bb0dd2c8..00000000 --- a/dev/tools/univdot +++ /dev/null @@ -1,49 +0,0 @@ -#!/bin/sh - -usage() { - echo "" - echo "usage: univdot [INPUT] [OUTPUT]" - echo "" - echo "takes the output of Dump Universes \"file\" command" - echo "and transforms it to the dot format" - echo "" - echo "Coq> Dump Universes \"univ.raw\"." - echo "" - echo "user@host> univdot univ.raw | dot -Tps > univ.ps" - echo "" -} - - -# these are dot edge attributes to draw arrows corresponding -# to > >= and = edges of the universe graph - -GT="[color=red]" -GE="[color=blue]" -EQ="[color=black]" - - -# input/output redirection -case $# in - 0) ;; - 1) case $1 in - -h|-help|--help) usage - exit 0 ;; - *) exec < $1 ;; - esac ;; - 2) exec < $1 > $2 ;; - *) usage - exit 0;; -esac - - -# dot header -echo 'digraph G {\ - size="7.5,10" ;\ - rankdir = TB ;' - -sed -e "s/^\([^ =>]\+\) > \([^ =>]\+\)/\1 -> \2 $GT/" \ - -e "s/^\([^ =>]\+\) >= \([^ =>]\+\)/\1 -> \2 $GE/" \ - -e "s/^\([^ =>]\+\) = \([^ =>]\+\)/\1 -> \2 $EQ/" \ -| sed -e "s/\./_/g" - -echo "}"
\ No newline at end of file |