Pure/ROOT.ML
cleaned comments;
removed extraneous 'print_depth 1';
replaced Basic_Syntax by BasicSyntax
added 'use "install_pp.ML"';
Pure/README
fixed comments;
Pure/POLY.ML
Pure/NJ.ML
make_pp: added fbrk;
Pure/install_pp.ML
replaced "Ast" by "Syntax";
Pure/sign.ML
added 'quote' to some error msgs;
#! /bin/sh
# xlisten -- start a program in one window and create a listener window
# environment variable $LISTEN specifies the file name
#create the file!
date > $LISTEN
xterm -geo 80x10+0+0 -T Listener -n Listener -e tail -f $LISTEN &
sleep 2
xterm -geo 80x45+0-0 -e teeinput $* &