public class ProofAsstGUI
extends java.lang.Object
ProofAsstGUI
class is the main user interface for the mmj2 Proof
Assistant feature.
A proof is represented in the GUI as a single text area, and the GUI knows nothing about the contents inside; all work on the proof is done elsewhere via mmj.pa.ProofAsst.java.
Note: ProofAsstGUI is single-threaded in the ProofAsst process which is triggered in BatchMMJ2. The RunParm that triggers ProofAsstGUI does not terminate until ProofAsstGUI terminates.
The main issues dealt with in the GUI have to do with doing all of the screen updating code on the Java event thread. Unification is performed using a separate thread which "calls back" to ProofAsstGUI when/if the Unification process is complete. (As of February 2006, the longest theorem unification computation is around 1/2 second.)
Modifier and Type | Class and Description |
---|---|
class |
ProofAsstGUI.RequestThreadStuff |
Modifier and Type | Field and Description |
---|---|
javax.swing.JFrame |
mainFrame |
Constructor and Description |
---|
ProofAsstGUI()
Default constructor used only in test mode when ProofAsstGUI invoked
directly from command line.
|
ProofAsstGUI(ProofAsst proofAsst,
ProofAsstPreferences proofAsstPreferences,
TheoremLoader theoremLoader)
Normal constructor for setting up ProofAsstGUI.
|
Modifier and Type | Method and Description |
---|---|
boolean |
cancelRequestAction() |
<T extends java.lang.Enum<T>> |
enumSettingAction(Setting<T> setting,
java.lang.String list,
java.lang.String prompt) |
int |
getCurrProofMaxSeq()
Get sequence number of Proof Worksheet theorem.
|
javax.swing.JFrame |
getMainFrame() |
MMTFolder |
getNewMMTFolder() |
static void |
main(java.lang.String[] args)
Test code to invoke GUI from command line.
|
boolean |
newGeneralSearch(java.lang.String s) |
boolean |
refineAndShowResults() |
<T> java.awt.event.ActionListener |
repromptAction(java.lang.String prompt,
java.util.function.Supplier<?> initial,
java.util.function.Predicate<java.lang.String> validator) |
<T> java.awt.event.ActionListener |
repromptAction(java.util.function.Supplier<java.lang.String> prompt,
java.util.function.Supplier<?> initial,
java.util.function.Predicate<java.lang.String> validator) |
boolean |
reshowProofAsstGUI() |
boolean |
reshowSearchOptions() |
boolean |
reshowSearchResults() |
boolean |
searchAndShowResults() |
mmj.pa.ProofAsstGUI.Request |
searchChoiceAction(StepRequest.StepRequestType type) |
boolean |
searchOptionsMinusButton() |
boolean |
searchOptionsPlusButton() |
boolean |
searchResultsMinusButton() |
boolean |
searchResultsPlusButton() |
void |
setCurrProofMaxSeq(int currProofMaxSeq)
Set sequence number of Proof Worksheet theorem.
|
void |
setCursorToStartOfMessageArea()
Positions the input caret to start of message text area and scrolls
viewport to ensure that the start of the message text area is visible.
|
void |
showMainFrame()
Show the GUI's main frame (screen).
|
boolean |
startRequestAction(mmj.pa.ProofAsstGUI.Request r) |
mmj.pa.ProofAsstGUI.Request |
unificationAction(boolean renumReq,
boolean noConvertWV,
PreprocessRequest preprocessRequest,
StepRequest stepRequest,
TLRequest tlRequest) |
boolean |
unifyWithStepSelectorChoice(StepRequest stepRequest) |
public ProofAsstGUI()
public ProofAsstGUI(ProofAsst proofAsst, ProofAsstPreferences proofAsstPreferences, TheoremLoader theoremLoader)
proofAsst
- ProofAsst objectproofAsstPreferences
- variable settingstheoremLoader
- mmj.tl.TheoremLoader objectpublic int getCurrProofMaxSeq()
Equals MObj.seq if proof theorem already exists. Otherwise, set to LOC_AFTER stmt sequnce + 1 if LOC_AFTER input (else Integer.MAX_VALUE).
public void setCurrProofMaxSeq(int currProofMaxSeq)
Equals MObj.seq if proof theorem already exists. Otherwise, set to LOC_AFTER stmt sequnce + 1 if LOC_AFTER input (else Integer.MAX_VALUE).
currProofMaxSeq
- number of Proof Worksheet theorem.public boolean unifyWithStepSelectorChoice(StepRequest stepRequest)
public boolean newGeneralSearch(java.lang.String s)
public boolean searchAndShowResults()
public boolean refineAndShowResults()
public boolean reshowSearchOptions()
public boolean reshowSearchResults()
public boolean reshowProofAsstGUI()
public boolean searchOptionsPlusButton()
public boolean searchOptionsMinusButton()
public boolean searchResultsPlusButton()
public boolean searchResultsMinusButton()
public javax.swing.JFrame getMainFrame()
public <T extends java.lang.Enum<T>> java.awt.event.ActionListener enumSettingAction(Setting<T> setting, java.lang.String list, java.lang.String prompt)
public <T> java.awt.event.ActionListener repromptAction(java.lang.String prompt, java.util.function.Supplier<?> initial, java.util.function.Predicate<java.lang.String> validator)
public <T> java.awt.event.ActionListener repromptAction(java.util.function.Supplier<java.lang.String> prompt, java.util.function.Supplier<?> initial, java.util.function.Predicate<java.lang.String> validator)
public mmj.pa.ProofAsstGUI.Request unificationAction(boolean renumReq, boolean noConvertWV, PreprocessRequest preprocessRequest, StepRequest stepRequest, TLRequest tlRequest)
public mmj.pa.ProofAsstGUI.Request searchChoiceAction(StepRequest.StepRequestType type)
public MMTFolder getNewMMTFolder()
public boolean startRequestAction(mmj.pa.ProofAsstGUI.Request r)
public boolean cancelRequestAction()
public void setCursorToStartOfMessageArea()
This is called only after updates to an existing AuxFrameGUI screen. It is automatically invoked during the initial display sequence of events..
public void showMainFrame()
public static void main(java.lang.String[] args)
args
- String array holding command line parms