On Thu, 5 Sep 2013, Florian Haftmann wrote:
I also observed that if you use sledgehammer as old-style keyword, the
proof text is inserted after instead of just replacing
This goes back to Isabelle/a0db255af8c5 from 1 month ago:
sledgehammer sendback always uses Markup.padding_command: sensible
default for most practical applications -- old-style in-line replacement
is superseded by auto mode or panel;
back to Normal mode: with output_result it is sufficient to determine
TTY vs. PIDE operation;
I've just got entangled into "too many modes", even nested ones. So I've
just made a clear cut, at the cost of loosing some former features, but
they were intermediate anyway until a proper control panel would arrive.
The "too many modes" problem has already become a new Isabelle insider
jargon expression in the past few months. (It needs to be distinguished
from "too many notes" from Amadeus.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
