#441 disable electric keys if current line indented manually

closed-fixed
None
6
2012-05-15
2012-05-05
No

I would like to fix these electric keys problems definitely. Vampire wrote once an extremely long post in which the gold idea is hidden:
http://jedit.9.n6.nabble.com/Indentation-problems-in-Python-tp1817874p1817919.html

Shortly speaking: electric keys should be disabled after user manually indented the current line. Does it have any disadvantages? I plan to introduce it as another smart mode.

My idea for implementation is to store the lastManuallyIndented line as a private buffer field. If it matches the current line, the electric keys won't work.

Discussion

  • Jarek Czekalski

    Jarek Czekalski - 2012-05-13

    The idea get materialized. I attach a patch that is in alpha stage of testing. However I would like to get your feedback about the design.

    1. JEditBuffer gets new public method:
    public void manualIndentationDone(int line)
    * Called by user interface layer to notify the buffer that manual
    * indentation of the given line took place.
    * Buffer needs that information for proper handling of
    * the electric keys in smart DMI mode.
    * A call to this method must be done inside the {@link #writeLock}.

    2. manualIndentationDone is called by TextArea methods that perform tasks like shiftIndentRight. Those methods should have used writeLock anyway, but they didn't. I added buffer.writeLock() to them.

    lastManIndLine member of JEditBuffer is not int, as I initially thought, but Position. int would fail if line insertions/removals were done before the given line, while Position is resistant to such actions. Position interface is also used for built-in markers.

     
  • Jarek Czekalski

    Jarek Czekalski - 2012-05-15
    • status: open --> closed-fixed
     

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks