Hello, It seems that there once was support for builtin functions defined by a front end. This is still a useful idea (see e.g. PR24777) but it looks like there are no frontend built-in functions anymore. At least, a grep for BUILT_IN_FRONTEND gives no meaningful results. There's a hint that it may have worked, long ago, in ChangeLog-2000. But there is no documentation whatsoever about how BUILT_IN_FRONTEND is supposed to work.
Does anyone know how BUILT_IN_FRONTEND should work, what one has to do to define a front-end built-in function? Examples? Any idea if there ever was a front end that used this feature? Ciao! Steven