void PushPop(function f)
Performs function f between GL.glPushMatrix and GL.glPopMatrix calls.
PushPop() { GL.glTranslate( 0.01, -0.9, 0.0 ); write_text( "Press esc to quit" ); };