Wed, 12 Mar 2014 22:57:50 +0100 tuned signature -- clarified module name;
wenzelm [Wed, 12 Mar 2014 22:57:50 +0100] rev 56072
tuned signature -- clarified module name;
Wed, 12 Mar 2014 22:44:55 +0100 added ML antiquotation @{here};
wenzelm [Wed, 12 Mar 2014 22:44:55 +0100] rev 56071
added ML antiquotation @{here};
Wed, 12 Mar 2014 22:41:04 +0100 ML_Context.check_antiquotation still required;
wenzelm [Wed, 12 Mar 2014 22:41:04 +0100] rev 56070
ML_Context.check_antiquotation still required;
Wed, 12 Mar 2014 21:58:48 +0100 simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm [Wed, 12 Mar 2014 21:58:48 +0100] rev 56069
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 +10000 tip