Hi,
At first time, I must say Thank You Very Much the support for this forgotten(?)
extension!
(I hope I am not The One user who use it...)
I didn't find any error that could have been caused by your great works.
I know, the BSE will never be a full-featured IDE, but maybe "we" can develop a
bi
fast and furious Mike! nicely done.. sunny regards ede
On 13.06.2020 15:03, michael michaud wrote:
> János
>
> I pushed the source code to our plugin repository, and hopefully, fixed the
> different points you mentionned. Please, try a new release from r6335. Note
> that I've also upgradded the
János
I pushed the source code to our plugin repository, and hopefully, fixed the
different points you mentionned. Please, try a new release from r6335. Note
that I've also upgradded the two dependencies without much testing (buoy for
the UI and beanshell for the language interpreter).
---
*
hey Mike,
yeah please provide the sources at least as they match up the current extension
we provide with PLUS. that helps in checking what's going on and actually we
are obliged by the GPL to do so for everything we distribute under it.
hope this finds you well ..ede
On 10.06.2020 13:58, mich
Thanks for the suggestion,
The beanshell editor is a very old plugin. The text editor is taken from an
even older version of JEdit, a very nice text editor, quite popular at this
time. Unfortunately, I never committed the source, but I still have it. I'll
check if I can make the police more acce
I don't have the source of the BeanShell Script Editor unfortunately,
otherwise I would have tried to do something... Maybe... Unfortunately I am
newbie in Java so I cannot know what I can do and what I cannot.
I has opened the
"c:\OpenJUMP-20200126-r6224-PLUS\lib\ext\bsheditor4jump-0.2.4.jar"
@kjt btw. where did you find the sources? they are not in our svn as far as i
can see.
@Mike do you maintain them somewhere else? ..ede
On 10.06.2020 11:27, kjt via Jump-pilot-devel wrote:
> In my oppinion the Font has been defined at BeanShellEditor.class in the
> fr.michaelm.bsheditor package
just to be clear. you want to change during runtime, not recompile the
extension? ..ede
On 10.06.2020 11:27, kjt via Jump-pilot-devel wrote:
> In my oppinion the Font has been defined at BeanShellEditor.class in the
> fr.michaelm.bsheditor package:
> 437. row: |this.outputTextArea.setFont(new Fo
In my oppinion the Font has been defined at BeanShellEditor.class in the
fr.michaelm.bsheditor package:
437. row: `this.outputTextArea.setFont(new Font("Monospaced", 0, 12));`
Can I modify anyway...?
---
** [support-requests:#7] BeanShell Script Editor properties**
**Status:** open
**Labels:**
The source code it probably here
https://sourceforge.net/p/jump-pilot/code/HEAD/tree/core/trunk/src/com/vividsolutions/jump/workbench/ui/plugin/BeanShellPlugIn.java
but I am not good enough att reading the code to tell where the font is either
set or perhaps leaved as default.
---
** [suppo
---
** [support-requests:#7] BeanShell Script Editor properties**
**Status:** open
**Labels:** beanshell beanshell script editor bsheditor4jump properties
**Created:** Wed Jun 10, 2020 08:08 AM UTC by kjt
**Last Updated:** Wed Jun 10, 2020 08:08 AM UTC
**Owner:** nobody
I would like to chan
11 matches
Mail list logo
