Isabelle has a sophisticated concrete syntax mechanism which makes it difficult to add annotations to connect the displayed output back to the internal abstract syntax. This issue needs to be solved to support proof-by-pointing (and other features) in Isabelle. A patch by Burkhart Wolff providing term structure annotations for a previous release of Isabelle may be useful here. To implement proof-by-pointing itself, tactics using the gesture information must be written.
Skills: Some understanding of Isabelle implementation, co-operation with the Isabelle developers to get Isabelle modifications incorporated. Skill in writing Isabelle tactics. Minimal Emacs Lisp knowledge.
Proposer: David Aspinall.