[ jEdit-devel ] Indent and tab are not the same thing

[Alan M. <ala...@op...>]

I use a two-column indent, but setting the tabSize property
to 2 for auto-indenting also causes tab characters to be
expanded to 2, which is usually not correct.  I've made some
changes so that tabs and indents are independent of each other.
The affected modules are included in the attached jar file,
with comments ('//am') wherever I made a change (often just
replacing the word 'indent' with 'tabSize').

Before you run this code, you'll have to create some new properties:

in jedit.props,     'buffer.indent=2'  (or 4 or 8)
in jedit_gui.props, 'options.editor.indent=Indent:'
       (or whatever label you want for the combobox)

So waddaya think?


--Alan