[isabelle-dev] NEWS: undefined ML expression

[Makarius]

*** ML ***

* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).

(Note that we already have a function called "undefined" for several 
years.)


This refers to Isabelle/53e32a9b66b8.  The idea to allow special shortcuts 
in Isabelle/ML is at least as old as the antiquotation syntax, e.g. see 
@{assert} or @{print}.

The recent introduction of \<^name>cartouche as short form for
@{name cartouche} has been pushed a bit further: \<^name> without 
cartouche argument abbreviates just @{name} (see Isabelle/3591274c607e).
So @{undefined} could be written succinctly as \<^undefined>.

The remaining problem was the Unicode rendering of \<^undefined>. I was 
first thinking of ⬚ (0x2b1a) but now it came out as the somewhat 
undefined ❖ (0x2756), which is a bit more visible in the text

Also note that there is a general side-condition: already assigned 
Isabelle symbols like \<hole> cannot be re-used as control symbols like 
\<^undefined>.


Since these control forms in document or ML source are formal 
antiquotations, the PIDE markup helps users to find out what they actually 
mean. Nonetheless, they need to be used sparingly, or Isabelle/ML could 
degrade into a version of APL.


 	Makarius