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?
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"));
}
}
});