| changeset 40893 | 7d88ebdce380 |
| parent 29143 | 72c960b2b83e |
| child 48515 | 3e17f343deb5 |
| 40892:6f7292b94652 | 40893:7d88ebdce380 |
|---|---|
86 } |
86 } |
87 |
87 |
88 function extract_syms () |
88 function extract_syms () |
89 { |
89 { |
90 perl -n \ |
90 perl -n \ |
91 -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ |
91 -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ |
92 "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst" |
92 "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst" |
93 perl -n \ |
93 perl -n \ |
94 -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \ |
94 -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \ |
95 "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst" |
95 "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst" |
96 } |
96 } |