JUMP-NEXT-WINDOWJUMP-NEXT-WINDOW cycles the cursor through all the open proof and term windows, except the ML-top-loop window. JUMP-MLJUMP-ML moves the Nuprl cursor to the ML top-loop.
