> Despite such routine improvements, many users will probably just stick to old > habits from the TTY age, and put the sledgehammer command into the text. (Are > there remaining uses of this ancient form? Or are there still pending > problems with the current Sledgehammer panel?)
I don’t think such uses of essentially diagnostic commands should go away, even if the corresponding panel works perfectly. I find typing in a diagnostic command usually much faster and less disruptive of the workflow than finding a panel in a list of tabs, and using the mouse to move focus there. Even though we have the very nice command-click for theorems etc, I still find myself using the thm command semi-regularly, just because I don’t want to pick up the mouse, or I want to leave in the command to remind myself of something, or I want to see the theorem in the context of where I’m trying to use it instead of were it is define. Sledgehammer is a slightly different case, because it often takes longer, but even here I still sometimes prefer the text to the graphical interface when I’m just using it to find a theorem. Panels are clearly better for beginners, and I do myself much appreciate them for things I don’t do often, but I think we should continue to support both modes of interaction so that people can do what suits their workflow best. Cheers, Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
