explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;
#!/bin/bash
#
# make_mlyacclib - Generates Isabelle-friendly version of ML-Yacc's library.
#
# This code is based on that used in src/Tools/Metis to adapt Metis for
# use in Isabelle.
MLYACCDIR=./ml-yacc
MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"
echo "Cleaning"
rm -f ml_yacc_lib.ML
echo "Generating ml_yacc_lib.ML"
(
cat <<EOF
(******************************************************************)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(******************************************************************)
print_depth 0;
(*
This file is generated from the contents of ML-Yacc's lib directory.
ML-Yacc's COPYRIGHT-file contents follow:
EOF
perl -pe 'print " ";' ml-yacc/COPYRIGHT
echo "*)"
for FILE in $MLYACCLIB_FILES
do
echo
echo "(**** Original file: $FILE ****)"
echo
echo -e " $FILE" >&2
perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
-e 's/Unsafe\.(.*)/\1/g;' \
-e 's/\bconcat\b/String.concat/g;' \
-e 's/(?<!List\.)foldr\b/List.foldr/g;' \
-e 's/\bfoldl\b/List.foldl/g;' \
-e 's/val print = fn s => TextIO\.output\(TextIO\.stdOut,s\)$//g;' \
-e 's/\bprint\b/TextIO.print/g;' \
$MLYACCDIR/lib/$FILE
done
cat <<EOF
;
print_depth 10;
EOF
) > ml_yacc_lib.ML