wenzelm [Sat, 09 Dec 2006 18:05:40 +0100] rev 21721
abbrevs: print original rhs;
wenzelm [Sat, 09 Dec 2006 18:05:39 +0100] rev 21720
abbreviate: always authentic, force expansion of internal abbreviations;
tuned signature;
tuned;
wenzelm [Sat, 09 Dec 2006 18:05:38 +0100] rev 21719
ML_Syntax.reserved(_names);
wenzelm [Sat, 09 Dec 2006 18:05:37 +0100] rev 21718
TermSyntax.abbrev;
wenzelm [Sat, 09 Dec 2006 18:05:36 +0100] rev 21717
added antiquotation abbrev;
wenzelm [Sat, 09 Dec 2006 18:05:34 +0100] rev 21716
added print_abbrevs;
wenzelm [Fri, 08 Dec 2006 23:25:54 +0100] rev 21715
tuned use_text;
eval command line: skip over -q option;
wenzelm [Fri, 08 Dec 2006 23:25:53 +0100] rev 21714
added 'help' command (same of 'print_commands');
wenzelm [Fri, 08 Dec 2006 23:25:52 +0100] rev 21713
more careful evaluation of ML text, prevents spurious output;
wenzelm [Fri, 08 Dec 2006 23:25:50 +0100] rev 21712
date: forcing LC_ALL=C prevents funny file names;