andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

Avoid hard tabulators? #50

Open makarius opened 11 years ago

makarius commented 11 years ago

Is there a way to make the Eclipse editor avoid hard tabulars by default?

There is a long story behind all that, and current Isabelle formally interprets tab as an alias of a single space, as lowest common denominator. Even that is apt to cause confusion, and I still hope to be able to discontinue tabulators in Isabelle sources at some point.

Incidently, it was David Aspinall experimenting with PGIP and PGEclipse in 2003/2004, who first proposed to make the tabbing always explicit via spaces, to avoid problems with all these different interpretations imposed by the surrounding editor framework.