*** 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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
