NEWS: Multiple hyperlinks in PIDE

[Makarius]

*** General ***

* Formal entities record more position information, from the history of
locale interpretations etc. This results in multiple PIDE markup, which
can be displayed to end-users as hyperlinks with multiple choices.


*** Isabelle/jEdit Prover IDE ***

* The jEdit action "goto-entity" has been superseded by "follow-link",
while retaining the keyboard shortcut CS+d. The new action is more
general: it uses the same notion of link as C-hover-click via mouse.
Minor INCOMPATIBILITY.

* Tooltip messages render formal entities with additional PIDE markup,
to distinguish multiple def-positions due to locale interpretations etc.


This refers to Isabelle/ad96a992ab53.


	Makarius