Re: [isabelle] 2014-RC1 issues
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] 2014-RC1 issues
- From: Makarius <makarius at sketis.net>
- Date: Sat, 2 Aug 2014 20:13:56 +0200 (CEST)
- Cc: Lars Noschinski <noschinl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <1406791217.2398.94.camel@lapbroy33>
- References: <1406708816.2398.53.camel@lapbroy33> <alpine.LNX.firstname.lastname@example.org> <53D9E56A.email@example.com> <1406791217.2398.94.camel@lapbroy33>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Thu, 31 Jul 2014, Peter Lammich wrote:
On the topic of the query panel: Some time in the future, I'd like to
see the equivalent of the jEdit action bar (or, to phrase it
differently, a "general" query panel) for Isabelle, where I enter an
arbitrary (diagnostic) command and get the output in the panel.
I think this was called "issue prover command" in PG ("Ctrl-c v" in
standard config), and I used it from time to time. It only worked for
commands that did not change the prover state, e.g., for all diagnostic
Such a mini command-line within Query is an obvious extension, but there
are also conceptual differences. There is no need to restrict it to
diagnostic command, because it is all stateless anyway. There is a need
to wrap up the hypothetical "script" a bit differently, to avoid spilling
of messages (wranings etc.) in the wrong place. This is why it is not
done yet -- the panel is new in the coming release anyway.
In jEdit this has been replaced by the more heavyweight query-panels
Again, and hopefully the last time, a quote from the Isabelle/jEdit
\item [jEdit] is a sophisticated text editor implemented in Java
\item [Isabelle/jEdit] is the main example application of the PIDE
framework and the default user-interface for Isabelle
If you need a short name for the Prover IDE, you can say "PIDE" -- it is
even easier to pronounce (and spell) than "jEdit". Yet another
alternative is to say just "Isabelle", according to the toplevel
Concerning the perceived heavyweightedness of the query panel: it is
actually relative simple, taking the whole conceptual complexity of
timeless/stateless asynchronous parallel document processing into account.
In contrast, issuing a single command on the spot is only simple under the
assumption of an existing TTY loop, which has its own complexities. Once
the TTY loop can be removed from Isabelle, great weights will disappear
from the overall system implementation.
that only work for a small subset of the diagnostic commands, and
extending them to new commands is quite a big effort.
The query panel is based on a general concept of query operation, which
are more flexible than old-style diagnostic commands, but also simpler.
The "Print Context" tab in the Query panel is a restricted application of
the general principle. The following one-liner installs a new item to be
printed there (without taking any arguments apart from the implicit
Print_Operation.register "test" "test output" (fn st => [Pretty.str "test"])
After emitting that ML snippet in PIDE, the Query panel needs to be
re-docked and will then show another checkbox for "test" than can be
activated on demand.
This archive was generated by a fusion of
Pipermail (Mailman edition) and