src/Pure/PIDE/active.ML
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
less more (0) tip