[ jEdit-devel ] [ jedit-Bugs-426001 ] changing text characteristics

[<no...@so...>]

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