steve
/
factor
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

forgot jedit metadata

cvs
Slava Pestov 2004-08-08 02:30:33 +00:00
parent 273d53fe48
commit f4c239a992
2 changed files with 36 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
actions.xml Normal file
View File

@ -0,0 +1,24 @@
<?xml version="1.0"?>
<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
<ACTIONS>
<ACTION NAME="factor-eval-selection">
<CODE>
sel = textArea.selectedText;
if(sel == null)
view.toolkit.beep();
else
factor.jedit.FactorPlugin.eval(view,sel);
</CODE>
</ACTION>
<ACTION NAME="factor-run-file">
<CODE>
buffer.save(view,null);
factor.jedit.FactorPlugin.eval(view,
"\""
+ MiscUtilities.charsToEscapes(buffer.path)
+ "\" run-file");
</CODE>
</ACTION>
</ACTIONS>

12
dockables.xml Normal file
View File

@ -0,0 +1,12 @@
<?xml version="1.0"?>
<!-- For jEdit plugin -->
<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
<DOCKABLES>
<DOCKABLE NAME="factor">
new factor.listener.FactorListenerPanel(
factor.jedit.FactorPlugin.getInterpreter(view));
</DOCKABLE>
</DOCKABLES>