Moved font settings from Vertex to GraphView.
2 # Title: make-rulenames
3 # Author: Larry Paulson, Cambridge University Computer Laboratory
4 # Copyright 1990 University of Cambridge
6 #shell script for adding signature and val declarations to a rules file
7 # usage: make-rulenames <directory>
9 #Input is the file ruleshell.ML, which defines a theory.
13 #Rule lines begin with a line containing the word "extend_theory"
14 # and end with a line containing the word "get_axiom"
16 #Each rule name xyz must appear on a line that begins
18 # ENSURE THAT THE FIRST RULE LINE DOES NOT CONTAIN A "[" CHARACTER!
19 #The file RULESIG gets lines like val Eq_comp: thm
20 # These are inserted after the line containing the string INSERT-RULESIG
22 #The file RULENAMES gets lines like val Eq_comp = ax"Eq_comp";
23 # These are inserted after the line containing the string INSERT-RULENAMES
24 #The input file should define the function "ax" above this point.
26 set -eu #terminate if error or unset variable
27 if [ ! '(' -d $1 -a -f $1/ruleshell.ML ')' ]; \
28 then echo $1 is not a suitable directory; exit 1; \
30 sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/ val \1: thm/p' $1/ruleshell.ML > RULESIG
31 sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/val \1 = ax"\1";/p' $1/ruleshell.ML > RULENAMES
32 sed -e '/INSERT-RULESIG/ r RULESIG
33 /INSERT-RULENAMES/ r RULENAMES' $1/ruleshell.ML > $1/.rules.ML
34 #WARNING: there must be no spaces after the filename in the "r" command!!