Re: [isabelle] 2014-RC1 issues

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 commands.

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 manual:

  \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 application name.

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 state):

  ML ‹
    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 MHonArc.