[isabelle-dev] NEWS: Isabelle/jEdit action "isabelle.goto-entity"

[Makarius]

On 18/12/2020 12:02, Lawrence Paulson wrote:
> I wish that some inspired student would put together a demo video or perhaps implement a “tip of the day” feature, because there are many many things (this will be yet another one) that are super useful almost impossible to discover. Your little trick for renaming bound variables is another; you demonstrated it to me but who could find it for himself?

Making videos is technically easy with OBS Studio (all platforms), but it
requires some work in producing a proper script and doing the performance well.

Moreover, videos need to be updated occasionally. I find it already difficult
to update the few screenshots in the Isabelle/jEdit manual (each could be a
short video sequence instead).


Maybe as a start, we can do live video sessions, something like informal
Isabelle workshops or tutorials.

I have already my own servers running: 2 Jitsi-Meet and 1 BigBlueButton, and
ran some small sessions quite successfully in the past few weeks.


	Makarius