Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Merge branch 'master' of https://github.com/calebegg/proof-pad

  • Loading branch information...
commit e3d75f0cd6a052f3a311b09220cca0450e2e3e2a 2 parents 1416f74 + 003802a
@PeterReid authored
View
9 src/org/proofpad/Acl2.java
@@ -555,9 +555,10 @@ public void run() {
fullSuccess &= !errorOccured;
fullOutput += response;
}
- outputQueue.add(new OutputEvent(response,
- errorOccured ? Repl.MsgType.ERROR : Repl.MsgType.SUCCESS));
-// System.out.println("RESPONSE: [[[" + response + "]]]");
+ if (!response.contains("DEFUN __TRACE-")) {
+ outputQueue.add(new OutputEvent(response,
+ errorOccured ? Repl.MsgType.ERROR : Repl.MsgType.SUCCESS));
+ }
sb = new StringBuilder();
errorOccured = false;
break;
@@ -707,7 +708,7 @@ private void admit(String code, Callback callback, boolean trace) {
} else {
traceExp.append(name);
}
- } else if (t.type == Token.IDENTIFIER && parser.functions.contains(t.getLexeme())) {
+ } else if (t.type == Token.IDENTIFIER && parser != null && parser.functions.contains(t.getLexeme())) {
traceExp.append("__trace-" + t.getLexeme());
} else {
traceExp.append(t.getLexeme());
View
3  src/org/proofpad/BuildWindow.java
@@ -76,8 +76,7 @@ public void build() {
builder.admit(
"(ccl:save-application \""
+ filename
- + "\" :toplevel-function #'__main__\n"
- + ":prepend-kernel t)",
+ + "\" :toplevel-function #'__main__ :prepend-kernel t)",
new Acl2.Callback() {
@Override
public boolean run(boolean success,
View
13 src/org/proofpad/CodePane.java
@@ -35,7 +35,7 @@
int widthGuide = -1;
private UndoManagerCreatedListener undoManagerCreatedListener;
private RUndoManager undoManager;
- private ActionListener helpAction;
+ private ActionListener lookUpAction;
public CodePane(final ProofBar pb) {
this.pb = pb;
@@ -55,7 +55,7 @@ public CodePane(final ProofBar pb) {
setBorder(BorderFactory.createEmptyBorder(0, leftMargin, 0, 0));
setTabSize(4);
setBackground(IdeWindow.transparent);
- helpAction = new ActionListener() {
+ lookUpAction = new ActionListener() {
@Override
public void actionPerformed(ActionEvent e) {
// First, check for a visible tooltip.
@@ -87,7 +87,12 @@ public void actionPerformed(ActionEvent e) {
t = t.getNextToken();
}
if (t != null) {
- String name = t.getLexeme();
+ String name;
+ try {
+ name = t.getLexeme();
+ } catch (NullPointerException ex) {
+ return;
+ }
if (name != null && Main.cache.getDocs().containsKey(name.toUpperCase())) {
try {
Desktop.getDesktop().browse(new URI("http://www.cs.utexas.edu/~moore/acl2/v4-3/"
@@ -330,6 +335,6 @@ public void SetUndoManagerCreatedListener(
public ActionListener getHelpAction() {
// TODO Auto-generated method stub
- return helpAction;
+ return lookUpAction;
}
}
View
3  src/org/proofpad/IdeWindow.java
@@ -318,7 +318,6 @@ public void actionPerformed(ActionEvent arg0) {
Matcher whitespace = Pattern.compile("^[ \t]*").matcher(lineStr);
whitespace.find();
int whitespaceLen = whitespace.group().length();
- System.out.println(whitespaceLen);
doc.remove(offset - eolLen, eolLen + whitespaceLen);
doc.insertString(offset - eolLen, eol, null);
} catch (BadLocationException e) { }
@@ -366,7 +365,7 @@ public void paintComponent(Graphics g) {
step2Y - lineHeight / 4);
g.drawString("3. Test them here.",
proofBar.getWidth() + 20,
- getHeight() - repl.inputLines * lineHeight - 30);
+ getHeight() - (int) repl.input.getPreferredScrollableViewportSize().getHeight() - 30);
}
});
tutorialAction = new ActionListener() {
View
31 src/org/proofpad/Main.java
@@ -7,7 +7,8 @@
import javax.swing.*;
import javax.swing.border.Border;
-import com.apple.eawt.AppEvent.OpenFilesEvent;
+import com.apple.eawt.*;
+import com.apple.eawt.AppEvent.*;
/* Proof Pad: An IDE for ACL2.
* Copyright (C) 2012 Caleb Eggensperger
@@ -84,8 +85,8 @@ public void uncaughtException(Thread t, Throwable e) {
logtime("Loaded cache");
if (IdeWindow.OSX) {
- com.apple.eawt.Application app = com.apple.eawt.Application.getApplication();
- app.setOpenFileHandler(new com.apple.eawt.OpenFilesHandler() {
+ Application app = Application.getApplication();
+ app.setOpenFileHandler(new OpenFilesHandler() {
@Override
public void openFiles(OpenFilesEvent e) {
for (Object file : e.getFiles()) {
@@ -94,16 +95,16 @@ public void openFiles(OpenFilesEvent e) {
}
}
});
- app.setAboutHandler(new com.apple.eawt.AboutHandler() {
+ app.setAboutHandler(new AboutHandler() {
@Override
- public void handleAbout(com.apple.eawt.AppEvent.AboutEvent e) {
+ public void handleAbout(AboutEvent e) {
new AboutWindow().setVisible(true);
}
});
- app.setQuitHandler(new com.apple.eawt.QuitHandler() {
+ app.setQuitHandler(new QuitHandler() {
@Override
- public void handleQuitRequestWith(com.apple.eawt.AppEvent.QuitEvent qe,
- com.apple.eawt.QuitResponse qr) {
+ public void handleQuitRequestWith(QuitEvent qe,
+ QuitResponse qr) {
for (Iterator<IdeWindow> ii = IdeWindow.windows.iterator(); ii.hasNext();) {
IdeWindow win = ii.next();
if (!win.promptIfUnsavedAndQuit(ii)) {
@@ -118,28 +119,28 @@ public void handleQuitRequestWith(com.apple.eawt.AppEvent.QuitEvent qe,
}
}
});
- app.setPreferencesHandler(new com.apple.eawt.PreferencesHandler() {
+ app.setPreferencesHandler(new PreferencesHandler() {
@Override
- public void handlePreferences(com.apple.eawt.AppEvent.PreferencesEvent arg0) {
+ public void handlePreferences(PreferencesEvent arg0) {
if (IdeWindow.prefsWindow == null) {
IdeWindow.prefsWindow = new PrefsWindow();
}
IdeWindow.prefsWindow.setVisible(true);
}
});
- app.addAppEventListener(new com.apple.eawt.AppForegroundListener() {
+ app.addAppEventListener(new AppForegroundListener() {
@Override
- public void appMovedToBackground(com.apple.eawt.AppEvent.AppForegroundEvent arg0) {
+ public void appMovedToBackground(AppForegroundEvent arg0) {
if (IdeWindow.windows.size() == 0 && !startingUp) {
System.exit(0);
}
}
@Override
- public void appRaisedToForeground(com.apple.eawt.AppEvent.AppForegroundEvent arg0) {}
+ public void appRaisedToForeground(AppForegroundEvent arg0) {}
});
- app.addAppEventListener(new com.apple.eawt.AppReOpenedListener() {
+ app.addAppEventListener(new AppReOpenedListener() {
@Override
- public void appReOpened(com.apple.eawt.AppEvent.AppReOpenedEvent arg0) {
+ public void appReOpened(AppReOpenedEvent arg0) {
if (IdeWindow.windows.size() == 0 && !startingUp) {
SwingUtilities.invokeLater(new Runnable() {
@Override
View
43 src/org/proofpad/MenuBar.java
@@ -38,6 +38,17 @@
public MenuBar(final IdeWindow parent) {
this.parent = parent;
+
+ final ActionListener prefsAction = new ActionListener() {
+ @Override
+ public void actionPerformed(ActionEvent e) {
+ if (IdeWindow.prefsWindow == null) {
+ IdeWindow.prefsWindow = new PrefsWindow();
+ }
+ IdeWindow.prefsWindow.setVisible(true);
+ }
+ };
+
JMenu menu = new JMenu("File");
JMenuItem item = new JMenuItem("New");
item.addActionListener(new ActionListener() {
@@ -223,7 +234,8 @@ public void actionPerformed(ActionEvent arg0) {
item.addActionListener(new RSyntaxTextAreaEditorKit.ToggleCommentAction());
item.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_SEMICOLON, modKey));
menu.add(item);
- item = new JMenuItem("Reindent");
+ item = new JMenuItem("Reindent " + (TITLE_CASE? 'S' : 's') + "elected " +
+ (TITLE_CASE ? 'L' : 'l') + "ines");
item.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_I, modKey));
if (parent == null) {
item.setEnabled(false);
@@ -231,23 +243,15 @@ public void actionPerformed(ActionEvent arg0) {
item.addActionListener(parent.reindentAction);
}
menu.add(item);
- if (!OSX) {
+ if (!OSX && !WIN) {
menu.addSeparator();
item = new JMenuItem("Preferences...");
- item.addActionListener(new ActionListener() {
- @Override
- public void actionPerformed(ActionEvent e) {
- if (IdeWindow.prefsWindow == null) {
- IdeWindow.prefsWindow = new PrefsWindow();
- }
- IdeWindow.prefsWindow.setVisible(true);
- }
- });
+ item.addActionListener(prefsAction);
menu.add(item);
}
add(menu);
/* ******* ACL2 Menu ******* */
- menu = new JMenu("ACL2");
+ menu = new JMenu("Tools");
item = new JMenuItem("Restart ACL2");
item.setEnabled(parent != null);
item.addActionListener(new ActionListener() {
@@ -279,7 +283,6 @@ public void actionPerformed(ActionEvent e) {
}
item.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_C, KeyEvent.CTRL_DOWN_MASK));
menu.add(item);
- menu.addSeparator();
item = new JMenuItem("Build");
item.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_B, modKey));
if (parent == null) {
@@ -288,7 +291,21 @@ public void actionPerformed(ActionEvent e) {
item.addActionListener(parent.buildAction);
}
menu.add(item);
+ menu.addSeparator();
+ item = new JMenuItem("Include " + (TITLE_CASE ? 'B' : 'b') + "ook...");
+ if (parent == null) {
+ item.setEnabled(false);
+ } else {
+ item.addActionListener(parent.includeBookAction);
+ }
+ menu.add(item);
add(menu);
+ if (WIN) {
+ item = new JMenuItem("Options...");
+ item.addActionListener(prefsAction);
+ menu.addSeparator();
+ menu.add(item);
+ }
/* ******* Window Menu (Mac only) ******* */
if (OSX) {
menu = new JMenu("Window");
View
3  src/org/proofpad/ProofBar.java
@@ -296,6 +296,9 @@ public void setLineHeight(int lineHeight) {
public void adjustHeights(java.util.LinkedList<Expression> newExps) {
this.expressions = newExps;
error = false;
+ for (UnprovenExp e : unprovenStates) {
+ e.status = Status.UNTRIED;
+ }
repaint();
}
View
97 src/org/proofpad/Repl.java
@@ -73,25 +73,25 @@ public Pair(T first, U second) {
}
private static final long serialVersionUID = -4551996064006604257L;
+ private static final int MAX_BOTTOM_HEIGHT = 100;
final Acl2 acl2;
private JPanel output;
JScrollBar vertical;
- final ArrayList<Pair<String,Integer>> history;
+ final ArrayList<String> history;
private CodePane definitions;
protected int historyIndex = 0;
boolean addedInputToHistory = false;
private Font font;
private List<JComponent> fontChangeList = new LinkedList<JComponent>();
CodePane input;
- private int inputHeightOneLine = -1;
- private JScrollPane inputScroller;
+ JScrollPane inputScroller;
private JSplitPane split;
private HeightChangeListener heightChangeListener;
- protected int inputLines = 1;
private JPanel bottom;
IdeWindow parent;
protected JButton trace;
protected JButton run;
+ private int oldNeededHeight = 26;
enum MsgType {
ERROR,
@@ -119,7 +119,7 @@ public void handleOutputEvent(OutputEvent e) {
this.definitions = definitions;
setBackground(Color.WHITE);
setOpaque(true);
- history = new ArrayList<Pair<String, Integer>>();
+ history = new ArrayList<String>();
output = new JPanel();
output.setLayout(new BoxLayout(output, BoxLayout.Y_AXIS));
output.setBackground(Color.WHITE);
@@ -163,7 +163,7 @@ public void actionPerformed(ActionEvent e) {
final String inputText = input.getText();
displayResult(inputText + "\n", MsgType.INPUT);
traceExp(inputText);
- history.add(new Pair<String, Integer>(inputText.trim(), inputLines));
+ history.add(inputText.trim());
historyIndex = history.size();
addedInputToHistory = false;
resetInput();
@@ -181,17 +181,17 @@ public void keyPressed(KeyEvent e) {
if (input.getCaretLineNumber() != 0) {
return;
}
- // TODO: Flash background color or something to indicate that the contents has changed? Maybe?
+ // TODO: Flash background color or something to indicate that the contents has
+ // changed? Maybe?
if (!input.getText().equals("") && !addedInputToHistory) {
- history.add(new Pair<String, Integer>(input.getText(), inputLines));
+ history.add(input.getText());
addedInputToHistory = true;
}
if (historyIndex > 0) {
historyIndex--;
- Pair<String, Integer> historyEntry = history.get(historyIndex);
- input.setText(historyEntry.first);
- inputLines = historyEntry.second;
- setBottomLines(Math.min(historyEntry.second, 5));
+ String historyEntry = history.get(historyIndex);
+ input.setText(historyEntry);
+ adjustBottomHeight();
input.setCaretPosition(0);
}
} else if (e.getKeyCode() == KeyEvent.VK_DOWN){
@@ -203,10 +203,9 @@ public void keyPressed(KeyEvent e) {
if (historyIndex == history.size()) {
resetInput();
} else {
- Pair<String, Integer> historyEntry = history.get(historyIndex);
- input.setText(historyEntry.first);
- inputLines = historyEntry.second;
- setBottomLines(Math.min(historyEntry.second, 5));
+ String historyEntry = history.get(historyIndex);
+ input.setText(historyEntry);
+ adjustBottomHeight();
input.setCaretPosition(input.getText().length());
}
}
@@ -214,6 +213,7 @@ public void keyPressed(KeyEvent e) {
}
@Override
public void keyTyped(KeyEvent e) {
+ adjustBottomHeight();
if (e.getKeyChar() == '\n') {
int parenLevel = 0;
for (Token t : input) {
@@ -229,11 +229,6 @@ public void keyTyped(KeyEvent e) {
if (parenLevel <= 0) {
e.consume();
runInputCode();
- } else {
- inputLines++;
- if (inputLines <= 6) {
- setBottomLines(inputLines);
- }
}
}
maybeEnableButtons();
@@ -248,23 +243,20 @@ public void keyTyped(KeyEvent e) {
split.setBottomComponent(bottomWrapper);
}
- void setBottomLines(int inputLines) {
- if (inputHeightOneLine == -1) {
- inputHeightOneLine = input.getHeight();
+ protected void adjustBottomHeight() {
+ System.out.println(oldNeededHeight);
+ int neededHeight = (int)input.getPreferredScrollableViewportSize().getHeight() + 2;
+ if (inputScroller.getHorizontalScrollBar().isVisible()) {
+ neededHeight += inputScroller.getHorizontalScrollBar().getHeight();
}
- int oldDividerLoc = split.getDividerLocation();
- int oldBottomDivisionHeight = split.getHeight() - oldDividerLoc;
- split.setDividerLocation(split.getHeight() - (inputHeightOneLine +
- (oldBottomDivisionHeight - input.getHeight()) + (inputLines - 1) * input.getLineHeight()));
- bottom.setSize(bottom.getWidth(), inputHeightOneLine + (inputLines - 1) * input.getLineHeight());
- int oldScrollerHeight = inputScroller.getHeight();
- int newScrollerHeight = inputHeightOneLine +
- (inputLines - 1) * input.getLineHeight() + 8;
- newScrollerHeight -= 6;
- Dimension newScrollSize = new Dimension(Short.MAX_VALUE,
- newScrollerHeight);
+ neededHeight = (neededHeight < MAX_BOTTOM_HEIGHT ? neededHeight : MAX_BOTTOM_HEIGHT);
+ split.setDividerLocation(split.getHeight() - neededHeight - 12);
+// bottom.setSize(bottom.getWidth(), neededHeight);
+// int oldScrollerHeight = inputScroller.getHeight();
+ Dimension newScrollSize = new Dimension(Short.MAX_VALUE, neededHeight);
inputScroller.setMaximumSize(newScrollSize);
- fireHeightChangedEvent(newScrollerHeight - oldScrollerHeight);
+ fireHeightChangedEvent(neededHeight - oldNeededHeight);
+ oldNeededHeight = neededHeight;
}
protected void fireHeightChangedEvent(int delta) {
@@ -284,7 +276,7 @@ void runInputCode() {
}
displayResult(input.getText() + "\n", MsgType.INPUT);
acl2.admit(input.getText(), null);
- history.add(new Pair<String, Integer>(input.getText().trim(), inputLines));
+ history.add(input.getText().trim());
if (history.size() > 500) {
for (int i = history.size(); i > 400; i--) {
history.remove(i);
@@ -301,23 +293,30 @@ public JPanel getOutput() {
void resetInput() {
input.setText("");
- if (inputHeightOneLine == -1) return;
- inputLines = 1;
- setBottomLines(1);
+ adjustBottomHeight();
}
- private static Pattern welcomeMessage = Pattern.compile(".*ACL2 comes with ABSOLUTELY NO WARRANTY\\..*");
- private static Pattern guardViolation = Pattern.compile("ACL2 Error in TOP-LEVEL: The guard for the function call (.*?), which is (.*?), is violated by the arguments in the call (.*?)\\..*");
- private static Pattern globalVar = Pattern.compile("ACL2 Error in TOP-LEVEL: Global variables, such as (.*?), are not allowed. See :DOC ASSIGN and :DOC @.");
- private static Pattern wrongNumParams = Pattern.compile("ACL2 Error in TOP-LEVEL: (.*?) takes (.*?) arguments? but in the call (.*?) it is given (.*?) arguments?\\..*");
- private static Pattern nonRec = Pattern.compile("Since (.*?) is non-recursive, its admission is trivial\\..*");
- private static Pattern trivial = Pattern.compile("The admission of (.*?) is trivial, using the relation O< .*");
- private static Pattern admission = Pattern.compile("For the admission of (.*?) we will use the relation O< .*");
+ private static Pattern welcomeMessage = Pattern.compile(".*ACL2 comes with ABSOLUTELY NO " +
+ "WARRANTY\\..*");
+ private static Pattern guardViolation = Pattern.compile("ACL2 Error in TOP-LEVEL: The guard " +
+ "for the function call (.*?), which is (.*?), is violated by the arguments in the " +
+ "call (.*?)\\..*");
+ private static Pattern globalVar = Pattern.compile("ACL2 Error in TOP-LEVEL: Global " +
+ "variables, such as (.*?), are not allowed. See :DOC ASSIGN and :DOC @.");
+ private static Pattern wrongNumParams = Pattern.compile("ACL2 Error in TOP-LEVEL: (.*?) " +
+ "takes (.*?) arguments? but in the call (.*?) it is given (.*?) arguments?\\..*");
+ private static Pattern nonRec = Pattern.compile("Since (.*?) is non-recursive, its admission " +
+ "is trivial\\..*");
+ private static Pattern trivial = Pattern.compile("The admission of (.*?) is trivial, using " +
+ "the relation O< .*");
+ private static Pattern admission = Pattern.compile("For the admission of (.*?) we will use " +
+ "the relation O< .*");
private static Pattern proved = Pattern.compile("Q.E.D.");
// TODO: Add these error messages (and others)
- // Undefined var
// Redefinition of func/reserved name
- private static Pattern undefinedFunc = Pattern.compile("ACL2 Error in TOP-LEVEL: The symbol (.*?) \\(in package \"ACL2\"\\) has neither a function nor macro definition in ACL2\\. Please define it\\..*");
+ private static Pattern undefinedFunc = Pattern.compile("ACL2 Error in TOP-LEVEL: The symbol " +
+ "(.*?) \\(in package \"ACL2\"\\) has neither a function nor macro definition in " +
+ "ACL2\\. Please define it\\..*");
public static String cleanUpMsg(String result) {
return cleanUpMsg(result, null, null);
}
Please sign in to comment.
Something went wrong with that request. Please try again.