[isabelle-dev] *** No column information -- cannot interpret tabulators

[Makarius]

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 
tabs.

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?


	Makarius