src/Pure/PIDE/editor.scala
Tue, 11 Aug 2015 17:00:16 +0200 wenzelm support hyperlinks with optional focus change;
less more (0) -10 -1 tip