[isabelle-dev] NEWS: Inner-syntax markup and declaration bundles

Makarius makarius at sketis.net
Thu Oct 10 16:32:20 CEST 2024


On 10/10/2024 15:36, Makarius wrote:
> 
> The markup for input was specifically requested by people from Linz, as a 
> prerequisite to make an "accessible" Prover IDE eventually. It means that 
> users without eyesight can explore types/terms/props by a tactile interface. 
> (A few years ago VSCode had made quite some noise about "accessibility", but 
> that has degraded a lot recently, so it is not an immediate answer to the 
> problem.)

Side-remark on this side-remark.

 From what I've learned in Linz 1 year ago, the main Open-Source product in 
this area is NVDA https://www.nvaccess.org (for Windows only).

The editor, whatever it is, needs to connect to that. There is even an 
official accessibility API Java, but I don't know if and how that works.


	Makarius



More information about the isabelle-dev mailing list