[isabelle-dev] Sledgehammer proof text insertion

[Makarius]

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