[isabelle-dev] *** No column information -- cannot interpret tabulators
makarius at sketis.net
Sun Aug 24 17:32:57 CEST 2008
On Sun, 24 Aug 2008, Makarius wrote:
> On Sun, 24 Aug 2008, Tobias Nipkow wrote:
> > I start getting these error messages when processing thy files with tabs in
> > them. Why? It is a pain to remove the tabs by hand.
> The system now takes source positions very seriously. Tabs are not really
> well-defined in that respect, but it should work most of the time. Can
> you produce an example where the error shows up?
In the meantime I have produced my own counterexample: it fails in Proof
General interactive mode only, and if tabs are used inside inner syntax. I
have now changed the internal untabification to fall back on a single
space as last resort.
Also note that the untabify command of Emacs replaces tabs by plain
spaces, avoiding problems in the first place. Moreover setting the
variable indent-tabs-mode to nil will stop Emacs from producing new hard
Concerning Proof General, it would be nice to get explicit source
positions at some point. Even with line count only it would already
greatly improve error messages, e.g. a syntax error within a term pointing
to the position where the parser stopped. When is PG 4.0 coming?
More information about the isabelle-dev