Naming the main JTextArea of jEdit from a BeanShell script

My goal is the following: Isabelle/jEdit is an extension of jEdit for the Isabelle theorem prover. I would like to get the typeset, syntax-highlighted version of my theory files to an image file programmatically, using a shell command, as they appear on the screen.

This is a follow-up to Calling into jEdit to get a bitmap of the rendered text where an author wrote a BeanShell script to translate a JTextArea into an image file. This is the script:

import java.awt.image.BufferedImage;
import javax.imageio.ImageIO;

img = new BufferedImage(textArea.getWidth(), textArea.getHeight(), BufferedImage.TYPE_INT_ARGB);
g = img.getGraphics();
textArea.paint(g);
g.dispose();
ImageIO.write(img, "png", new File(".../textArea.png"));

and I called that from the command line

$ isabelle jedit -j "-run=textarea-snapshot.bsh" MyTheory.thy

but the BeanShell script's textArea is undefined so I got an error.

So I should get the main JTextArea of jEdit to make this work.

As far as I understand it is created at

https://github.com/albfan/jEdit/blob/master/org/gjt/sp/jedit/gui/RegisterViewer.java#L78

contentTextArea = new JTextArea(10,20);

but it is not clear whether I can access it from a BeanShell script without modifying jEdit's code.

Could someone with jEdit experience answer how I could name this contentTextArea from my BeanShell script? Or, how could I solve my Original Goal?

Solution

The BeanShell script I gave you in that linked question was to take an image of an already running and existing jEdit instance. There textArea is exactly the way to access the text area.

If you run that script during a fresh startup of jEdit, it is executed too early and the text area does not yet exist.

If you want to do it like that, you need to write a more sophisticated script, that registers an EditBus component and thus can react to events like the view being activated.

Something along the lines of

import java.awt.image.BufferedImage;
import javax.imageio.ImageIO;

EditBus.addToBus(new EBComponent() {
    public void handleMessage(EBMessage message) {
        if ((message instanceof ViewUpdate) && (message.getWhat() == ViewUpdate.ACTIVATED)) {
            EditBus.removeFromBus(this);
            textArea = message.getView().getTextArea();
            img = new BufferedImage(textArea.getWidth(), textArea.getHeight(), BufferedImage.TYPE_INT_ARGB);
            g = img.getGraphics();
            textArea.paint(g);
            g.dispose();
            ImageIO.write(img, "png", new File("textArea.png"));
        }
    }
});