[isabelle] Output panel sometimes does not properly update with results of "try" or "sledgehammer"



Hi,

In Isabelle2016 I have noticed that the Output panel sometimes does
not update correctly when a sledgehammer or try command successfully
returns results.  For example, intermittently, on invoking "try", the
Output panel prints the usual

  "Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and
"nitpick"..."

message, but if any proof method invoked by try successfully finds a
proof this is not relayed to the user by another message appearing in
the panel, as one would expect, and as what usually happens.  Instead,
the user must notice that the try or sledgehammer command is now
underlined in grey in the Isabelle/jEdit editor pane, and the found
proof must be retrieved from the popup window that appears whilst
mouse hovering over the command.

(I'm not sure if this is the correct place to report apparent bugs or
unexpected behaviours --- is there an Isabelle bug tracker?)

Thanks,
Dominic




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.