-*- mode:outline -*-

* Things to do for Isabelle/Isar

See also ../todo for generic things to do, priority codes.

** C undo 'use' command: unlock corresponding ML file;

** C provide template for empty theory (or even just for Scratch.thy);

** C proper proof-by-pointing support (hard; needs major reworking of
Isabelle's pretty-printing subsystem);

** C tune behaviour of goals/response buffers (e.g. hide empty
response buffers when using 2 buffer model);

** D Combine with isa/ to get single Isabelle PG instance, somehow?
Then users could use both proof languages in the same session.

** D Fixup so that typing in shell buffer updates locked buffer status.
It works in Isabelle/classic, why not here?  (But users shouldn't
type in shell buffer, anyway).

** D support proof-next-error?