some refactoring
parent
c56ca0ca1f
commit
f6e3f24f90
|
@ -29,6 +29,9 @@ plugin.factor.jedit.FactorPlugin.menu=factor-listener \
|
|||
- \
|
||||
factor-extract-word \
|
||||
- \
|
||||
factor-infer-effect \
|
||||
factor-compile \
|
||||
- \
|
||||
factor-infer-effects \
|
||||
- \
|
||||
factor-restart
|
||||
|
@ -43,7 +46,9 @@ factor-edit.label=Edit word at caret
|
|||
factor-edit-dialog.label=Edit word...
|
||||
factor-usages.label=Word usages at caret
|
||||
factor-extract-word.label=Extract word...
|
||||
factor-infer-effects.label=Infer word stack effects...
|
||||
factor-infer-effect.label=Infer word stack effect
|
||||
factor-compile.label=Compile word at caret
|
||||
factor-infer-effects.label=Infer word stack effects
|
||||
factor-restart.label=Restart Factor
|
||||
|
||||
# SideKick stuff
|
||||
|
|
|
@ -38,48 +38,16 @@ import org.gjt.sp.jedit.textarea.JEditTextArea;
|
|||
import org.gjt.sp.jedit.*;
|
||||
import org.gjt.sp.util.Log;
|
||||
|
||||
public class WordPopup extends JWindow
|
||||
public class TextAreaPopup extends JWindow
|
||||
{
|
||||
private View view;
|
||||
private JTextArea preview;
|
||||
|
||||
//{{{ showWordPopup() method
|
||||
public static void showWordPopup(JEditTextArea textArea)
|
||||
//{{{ TextAreaPopup constructor
|
||||
public TextAreaPopup(JEditTextArea textArea, String text)
|
||||
{
|
||||
View view = GUIUtilities.getView(textArea);
|
||||
String def;
|
||||
|
||||
try
|
||||
{
|
||||
def = FactorPlugin.evalInWire(
|
||||
FactorPlugin.factorWord(view)
|
||||
+ " see").trim();
|
||||
}
|
||||
catch(IOException io)
|
||||
{
|
||||
def = io.toString();
|
||||
Log.log(Log.ERROR,WordPopup.class,io);
|
||||
}
|
||||
|
||||
WordPopup popup = new WordPopup(view,def);
|
||||
|
||||
int line = textArea.getCaretLine();
|
||||
String lineText = textArea.getLineText(line);
|
||||
int caret = textArea.getCaretPosition()
|
||||
- textArea.getLineStartOffset(line);
|
||||
int start = FactorPlugin.getWordStartOffset(lineText,caret);
|
||||
Point loc = textArea.offsetToXY(line,start);
|
||||
loc.y += textArea.getPainter().getFontMetrics().getHeight();
|
||||
SwingUtilities.convertPointToScreen(loc,textArea.getPainter());
|
||||
popup.setLocation(loc);
|
||||
popup.show();
|
||||
} //}}}
|
||||
|
||||
//{{{ WordPopup constructor
|
||||
public WordPopup(View view, String text)
|
||||
{
|
||||
super(view);
|
||||
this.view = view;
|
||||
super(GUIUtilities.getView(textArea));
|
||||
this.view = GUIUtilities.getView(textArea);
|
||||
preview = new JTextArea(text);
|
||||
preview.setEditable(false);
|
||||
getContentPane().add(BorderLayout.CENTER,new JScrollPane(preview));
|
||||
|
@ -91,6 +59,23 @@ public class WordPopup extends JWindow
|
|||
view.setKeyEventInterceptor(keyHandler);
|
||||
|
||||
GUIUtilities.requestFocus(this,preview);
|
||||
|
||||
positionAtCaret(textArea);
|
||||
setVisible(true);
|
||||
} //}}}
|
||||
|
||||
//{{{ positionAtCaret() method
|
||||
private void positionAtCaret(JEditTextArea textArea)
|
||||
{
|
||||
int line = textArea.getCaretLine();
|
||||
String lineText = textArea.getLineText(line);
|
||||
int caret = textArea.getCaretPosition()
|
||||
- textArea.getLineStartOffset(line);
|
||||
int start = FactorPlugin.getWordStartOffset(lineText,caret);
|
||||
Point loc = textArea.offsetToXY(line,start);
|
||||
loc.y += textArea.getPainter().getFontMetrics().getHeight();
|
||||
SwingUtilities.convertPointToScreen(loc,textArea.getPainter());
|
||||
setLocation(loc);
|
||||
} //}}}
|
||||
|
||||
//{{{ KeyHandler class
|
Loading…
Reference in New Issue