On Sun, 4 Aug 2013, Fabian Immler wrote:
I think it is a good idea to inform everyone here that a current
student's project is about to provide a bit more advanced user interface
for the find theorems functionality. It should be finished in two weeks
time.
So far I only know about the existence of the project, but nothing about
its contents.
I was about to ask about it today, since I have made some further progress
to get the concepts behind these query operations right:
changeset: 52865:02a7e7180ee5
user: wenzelm
date: Mon Aug 05 17:14:02 2013 +0200
files: src/Pure/PIDE/query_operation.ML src/Pure/ROOT
src/Pure/ROOT.ML src/Pure/Tools/find_theorems.ML
src/Tools/jEdit/lib/Tools/jedit src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/query_operation.scala
description:
slightly more general support for one-shot query operations via
asynchronous print functions and temporary document overlay;
Various fine points still need to be sorted out, both at the surface and
the bottom of it.
I have started thinking about a few advanced GUI aspect, e.g. completion
within the input text area, potentially also formal markup there. As a
general principle the GUI needs to work smoothly both for beginners and
experts. GUIs should not be toys.
PS: Next time I pass by find_theorems.ML, all the dead code will be
garbage collected.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
