Interface | Description |
---|---|
BaseSetting<T> | |
BaseSetting.JSONSerializable | |
BaseSetting.JSONSetting<T> | |
MMJException.ErrorContext |
An error context is an extra piece of information about the location of
the error, such as "Theorem X" or "Line 2".
|
ProofUnifier.PostUnifyHook | |
Serializer<T> | |
SessionStore.OnChangeListener<T> |
Class | Description |
---|---|
AuxFrameGUI |
A base class to display an auxiliary frame of information that is standalone
from a main application, for example a help page or a quick-and-dirty query
report.
|
AuxFrameGUI.FrameShower |
Inner class used to display the Frame later on the event queue thread.
|
CommentStmt | |
CompoundUndoManager |
This class will merge individual edits into a single larger edit.
|
DerivationStep |
DerivationStep represents proof steps that derive a new formula.
|
DistinctVariablesStmt |
DistinctVariablesStmt represents a single Metamath $d statement in a
ProofWorksheet.
|
EraseWffsPreprocessRequest |
EraseWffsPreprocessRequest implements a user request for an erasure operation
on non-QED Derivation Step formulas in a proof text area.
|
ErrorCode |
Error Codes used in mmj2
|
FooterStmt |
FooterStmt is simply the "$)" in column 1 of the last line of a proof.
|
GeneratedProofStmt |
GeneratedProofStatement is added automatically after successful unification.
|
HeaderStmt |
HeaderStmt represents the first line of the ProofWorksheet.
|
HelpGeneralInfoGUI |
Displays general information about the Proof Assistant GUI.
|
HighlightedDocument | |
HypothesisStep |
HypothesisStep represents a Logical Hypothesis of the Theorem being proved.
|
MacroManager |
Manages access to the WorkVarManager resource and processes Work Var
RunParms.
|
MacroStmt | |
MMJException.FormatContext | |
PaConstants |
(Most) Constants used in mmj.pa classes
|
PaConstants.StepContext | |
PaConstants.TheoremContext | |
PreprocessRequest |
PreprocessRequest implements a user request for an editing operation prior to
unification on a Proof Worksheet's text area.
|
ProofAsst |
The
ProofAsst , along with the rest of the mmj.pa package
provides a graphical user interface (GUI) facility for developing Metamath
proofs. |
ProofAsstCursor |
Simple data structure to hold caret/scroll params for the Proof Asst GUI.
|
ProofAsstGUI |
The
ProofAsstGUI class is the main user interface for the mmj2 Proof
Assistant feature. |
ProofAsstPreferences |
Holds user settings/preferences used by the Proof Assistant.
|
ProofStepStmt |
ProofStepStmt represents the commonalities of DerivationStep and
HypothesisStep.
|
ProofUnifier |
ProofUnifier is a separate class simply to break out the unification code
from everything else.
|
ProofWorksheet |
ProofWorksheet is generated from a text area (String) using ProofWorksheet
methods.
|
ProofWorksheetParser |
ProofWorksheetParser handles the details of iteration through 1 or more
ProofWorksheets input via String, File or Reader.
|
ProofWorkStmt |
General object representing an item on a ProofWorksheet.
|
RequestMessagesGUI |
Displays error messages from ProofAsst Unification.
|
SessionStore | |
Setting<T> | |
StepRequest |
StepRequest contains the StepSelector search results and is passed to the
ProofAsstGUI for use in generating the StepSelectorDialog.
|
StepSelectorDialog |
StepSelectorDialog is used by ProofAsstGUI to allow the user to choose from a
list of unifying assertions for a given proof step.
|
StepSelectorItem |
StepSelectorItem contains a single result obtained from the StepSelector
search.
|
StepSelectorResults |
StepSelectorResults contains the StepSelector search results and is passed to
the ProofAsstGUI for use in generating the StepSelectorDialog.
|
StepSelectorSearch |
StepSelectorSearch builds StepSelectorResults for a single derivation proof
step.
|
StepSelectorStore |
StepSelectorStore accumulates StepSelector results.
|
StepUnifier |
StepUnifier implements an algorithm based on Robinson's original unification
algorithm to unify two formulas.
|
UnifySubst |
UnifySubst is a data structure for use in proof unification.
|
WorksheetTokenizer | |
WorksheetTokenizer.Token |
Enum | Description |
---|---|
ErrorCode.ErrorLevel | |
MacroManager.CallbackType | |
MacroManager.ExecutionMode | |
PaConstants.DjVarsErrorStatus | |
PaConstants.DjVarsSoftErrors | |
PaConstants.IncompleteStepCursor |
Controls how cursor positioned after Unification if there are no errors
and at least one "incomplete" proof step: set cursor to First incomplete
proof step.
|
PaConstants.ProofFormat | |
PaConstants.UnificationStatus | |
StepRequest.StepRequestType |
Exception | Description |
---|---|
MMJException |
Superclass of all MMJ messages, for both info and errors.
|
ProofAsstException |
Custom exception for ProofAsst.
|