public class SettingChangeInteraction extends Interaction
Interaction.InteractionGraphicStyle
graphicalStyle
Constructor and Description |
---|
SettingChangeInteraction() |
SettingChangeInteraction(java.util.Properties settings,
InteractionListener.SettingType t) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getMarkdown() |
java.lang.String |
getMessage() |
java.util.Properties |
getSavedSettings() |
InteractionListener.SettingType |
getType() |
void |
reapply(WindowUserInterfaceControl uic,
Goal goal) |
void |
setMessage(java.lang.String message) |
void |
setSavedSettings(java.util.Properties savedSettings) |
java.lang.String |
toString() |
getCreated, getGraphicalStyle, isFavoured, setCreated, setFavoured
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getProofScriptRepresentation
public SettingChangeInteraction()
public SettingChangeInteraction(java.util.Properties settings, InteractionListener.SettingType t)
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String getMessage()
public void setMessage(java.lang.String message)
public java.util.Properties getSavedSettings()
public void setSavedSettings(java.util.Properties savedSettings)
public InteractionListener.SettingType getType()
public java.lang.String getMarkdown()
public void reapply(WindowUserInterfaceControl uic, Goal goal) throws java.lang.Exception
java.lang.Exception
Copyright © 2003-2019 The KeY-Project.