[isabelle-dev] NEWS: document antiquotation @{url}

Makarius makarius at sketis.net
Mon Dec 9 13:11:49 CET 2013


* Document antiquotation @{url} produces markup for the given URL,
which results in an active hyperlink within the text.


This refers to 3daeba5130f0.  Activation of hyperlinks in Isabelle/jEdit 
works via the recent Isabelle_System.open operation, which in turn is 
based on $ISABELLE_OPEN.

This has some potential for surprise, due to normal multi-platform 
insanity.  Any observations should be discussed here.


 	Makarius


More information about the isabelle-dev mailing list