On 2012-06-30, Vincent van Ravesteijn wrote: > Op 30-6-2012 15:17, Uwe Stöhr schreef: >> Am 30.06.2012 11:04, schrieb Vincent van Ravesteijn:
>>> 1. This must be next_next_token() >> I also thought this first. But as "\" is not found .asCharacter so >> that we have in case of "+\+" >> + \ + >> current_token skipped next_token() >> Using next_next_token() would not return the '\'. > Maybe we should change theCatcode list temporarily, but ok. You're right. As changing catcodes is what \verb and verbatim do, this seems the right thing to do. Günter
