Bugs item #426001, was opened at 2001-05-21 11:49
You can respond by visiting:
http://sourceforge.net/tracker/?func=detail&atid=100588&aid=426001&group_id=588
Category: text area and syntax packages
Group: normal bug
>Status: Closed
>Resolution: Fixed
Priority: 5
Submitted By: tony bigbee (adeveloper1)
Assigned to: Nobody/Anonymous (nobody)
Summary: changing text characteristics
Initial Comment:
After any compilation error (Java compile plugin with tools.jar in lib/ext), text coloring, bolding, and
characteristics of entire text buffer oscillate when when changing text. Using JDK 1.3.0_02,
Win2k, Win NT 4.0 SP5, and Jedit 3.1. Closing jedit and restarting "alleviates" problem.
The text switches from bold to unbold or vice versa as soon as I click any drop down menu in the
interface bar. Clicking in any particular area sometimes debolds some text after the compilation
error.
----------------------------------------------------------------------
>Comment By: Slava Pestov (spestov)
Date: 2001-06-30 19:25
Message:
Logged In: YES
user_id=2280
I don't know if you are still interested in getting jEdit to
work (it's been a month since this bug report...) but I
think I have fixed the bug. Try installing jEdit 3.2pre4,
then replace 'jedit.jar' with the one downloaded from this
location:
http://www.jedit.org/jedit.jar
----------------------------------------------------------------------
You can respond by visiting:
http://sourceforge.net/tracker/?func=detail&atid=100588&aid=426001&group_id=588
|
