src/Pure/PIDE/editor.scala
Tue, 11 Aug 2015 17:00:16 +0200 wenzelm support hyperlinks with optional focus change;
Wed, 09 Apr 2014 13:32:34 +0200 wenzelm avoid confusion about pointless cursor movement with external links;
Mon, 03 Mar 2014 12:54:12 +0100 wenzelm tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
less more (0) -10 -3 tip