Java Doc for KeYMediator.java in  » Testing » KeY » de » uka » ilkd » key » gui » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation 1.  6.0 JDK Core 2.  6.0 JDK Modules 3.  6.0 JDK Modules com.sun 4.  6.0 JDK Modules com.sun.java 5.  6.0 JDK Modules sun 6.  6.0 JDK Platform 7.  Ajax 8.  Apache Harmony Java SE 9.  Aspect oriented 10.  Authentication Authorization 11.  Blogger System 12.  Build 13.  Byte Code 14.  Cache 15.  Chart 16.  Chat 17.  Code Analyzer 18.  Collaboration 19.  Content Management System 20.  Database Client 21.  Database DBMS 22.  Database JDBC Connection Pool 23.  Database ORM 24.  Development 25.  EJB Server geronimo 26.  EJB Server GlassFish 27.  EJB Server JBoss 4.2.1 28.  EJB Server resin 3.1.5 29.  ERP CRM Financial 30.  ESB 31.  Forum 32.  GIS 33.  Graphic Library 34.  Groupware 35.  HTML Parser 36.  IDE 37.  IDE Eclipse 38.  IDE Netbeans 39.  Installer 40.  Internationalization Localization 41.  Inversion of Control 42.  Issue Tracking 43.  J2EE 44.  JBoss 45.  JMS 46.  JMX 47.  Library 48.  Mail Clients 49.  Net 50.  Parser 51.  PDF 52.  Portal 53.  Profiler 54.  Project Management 55.  Report 56.  RSS RDF 57.  Rule Engine 58.  Science 59.  Scripting 60.  Search Engine 61.  Security 62.  Sevlet Container 63.  Source Control 64.  Swing Library 65.  Template Engine 66.  Test Coverage 67.  Testing 68.  UML 69.  Web Crawler 70.  Web Framework 71.  Web Mail 72.  Web Server 73.  Web Services 74.  Web Services apache cxf 2.0.1 75.  Web Services AXIS2 76.  Wiki Engine 77.  Workflow Engines 78.  XML 79.  XML UI Java Java Tutorial Java Open Source Jar File Download Java Articles Java Products Java by API Photoshop Tutorials Maya Tutorials Flash Tutorials 3ds-Max Tutorials Illustrator Tutorials GIMP Tutorials C# / C Sharp C# / CSharp Tutorial C# / CSharp Open Source ASP.Net ASP.NET Tutorial JavaScript DHTML JavaScript Tutorial JavaScript Reference HTML / CSS HTML CSS Reference C / ANSI-C C Tutorial C++ C++ Tutorial Ruby PHP Python Python Tutorial Python Open Source SQL Server / T-SQL SQL Server / T-SQL Tutorial Oracle PL / SQL Oracle PL/SQL Tutorial PostgreSQL SQL / MySQL MySQL Tutorial VB.Net VB.Net Tutorial Flash / Flex / ActionScript VBA / Excel / Access / Word XML XML Tutorial Microsoft Office PowerPoint 2007 Tutorial Microsoft Office Excel 2007 Tutorial Microsoft Office Word 2007 Tutorial

Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.gui   Source Cross Reference   Class Diagram   Java Document (Java Doc)   java.lang.Object    de.uka.ilkd.key.gui.KeYMediator KeYMediator public class KeYMediator (Code) Inner Class :class KeYMediatorProofTreeListener extends ProofTreeAdapter Inner Class :class KeYMediatorProofListener implements RuleAppListener,AutoModeListener Inner Class :class KeYMediatorSelectionListener implements KeYSelectionListener Constructor Summary public   KeYMediator(Main mainFrame)      Method Summary public  void addAutoModeListener(AutoModeListener listener)      public  void addGUIListener(GUIListener listener)      public synchronized  void addKeYSelectionListener(KeYSelectionListener listener)      public  void addRuleAppListener(RuleAppListener listener)      public  void applyInteractive(RuleApp app, Goal goal)      Apply a RuleApp and continue with update simplification or strategy application according to current settings. public  boolean autoMode()      public  void changeNode(Node n)      public  Namespace choice_ns()      public  void closedAGoal()      public  boolean ensureProofLoaded()      public  boolean ensureProofLoadedSilent()      public synchronized  void fireModalDialogClosed(GUIEvent e)      public synchronized  void fireModalDialogOpened(GUIEvent e)      public synchronized  void fireShutDown(GUIEvent e)      Fires the shut down event. public synchronized  void freeModalAccess(Object src)      public  Namespace func_ns()      public  void generateTestCaseForSelectedNode()      public  long getAutomaticApplicationTimeout()      public  ListOfBuiltInRule getBuiltInRule(PosInOccurrence pos)      public  SetOfRuleApp getBuiltInRuleApplications(String name, PosInOccurrence pos)      public  KeYExceptionHandler getExceptionHandler()      public  ListOfTacletApp getFindTaclet(PosInSequent pos)      public  InteractiveProver getInteractiveProver()      Get the interactive prover. public  JavaInfo getJavaInfo()      public  int getMaxAutomaticSteps()      public  MetavariableDeliverer getMetavariableDeliverer()      public  ListOfTacletApp getNoFindTaclet()      public  NotationInfo getNotationInfo()      public  int getNrGoalsClosedByAutoMode()      public  Profile getProfile()      public  Proof getProof()      public  ProverTaskListener getProverTaskListener()      public  ReuseListener getReuseListener()      public  ListOfTacletApp getRewriteTaclet(PosInSequent pos)      public  Goal getSelectedGoal()      public  Node getSelectedNode()      public  Proof getSelectedProof()      public  KeYSelectionModel getSelectionModel()      public  Services getServices()      public  SetOfTacletApp getTacletApplications(Goal g, String name, PosInOccurrence p)      public  SetOfTacletApp getTacletApplications(Goal goal, String name, PosInOccurrence pos, TacletFilter filter)      public  ConstraintTableModel getUserConstraint()      public  void goalChosen(Goal goal)      public  Namespace heur_ns()      public  void indicateNoReuse()      public  void indicateReuse(ReusePoint p)      public static  void invokeAndWait(Runnable runner)      public  JFrame mainFrame()      public  void mark(Node n)      public  void markPersistent(Node n)      public  NamespaceSet namespaces()      public  void nonGoalNodeChosen(Node node)      public  void notify(NotificationEvent event)      public  void popupInformationMessage(Object message, String title)      public  void popupInformationMessage(Object message, String title, boolean modal)      Brings up a dialog displaying a message. public  void popupWarning(Object message, String title)      public  Namespace progVar_ns()      public  Namespace pv_ns()      public  void removeAutoModeListener(AutoModeListener listener)      public  void removeGUIListener(GUIListener listener)      public synchronized  void removeKeYSelectionListener(KeYSelectionListener listener)      public  void removeRuleAppListener(RuleAppListener listener)      public synchronized  void requestModalAccess(Object src)      public  void resetNrGoalsClosedByHeuristics()      public  boolean reuseInProgress()      public  void selectedBuiltInRule(BuiltInRule rule, PosInOccurrence pos)      public  void selectedTaclet(TacletApp tacletApp, PosInSequent pos)      public  boolean selectedTaclet(Taclet taclet, Goal goal, PosInOccurrence pos)      public  boolean selectedUseMethodContractRule(MethodContractRuleApp app)      public  void setAutomaticApplicationTimeout(long timeout)      public  void setBack()      Undo. public  void setBack(Node node)      public  void setBack(Goal goal)      public static  void setCenter(Component comp, Component parent)      Center a component within a parental component. Parameters:   comp - the component to be centered. Parameters:   parent - center relative to what. public static  void setCenter(Component comp)      Center a component on the screen. public  void setContinuousReuse(boolean b)      public  void setInteractive(boolean b)      Switches interactive mode on or off. public  void setMaxAutomaticSteps(int steps)      public  void setProof(Proof p)      public  void setResumeAutoMode(boolean b)      public  void setSimplifier(UpdateSimplifier s)      public  void setStupidMode(boolean b)      public  void showPreImage()      public  void showReuseState()      public  Namespace sort_ns()      public  void startAutoMode()      Start automatic application of rules on open goals. public  void startAutoMode(ListOfGoal goals)      Start automatic application of rules on specified goals. public  void startInterface(boolean fullStop)      public  void stopAutoMode()      Stop automatic application of rules. public  void stopInterface(boolean fullStop)      public  boolean stupidMode()      public  void testCaseConfirmation(String path)      public  void testCaseConfirmation(String path, int coverage)      public  Namespace var_ns()      public  ProofVisualization visualizeProof()      Constructor Detail KeYMediator public KeYMediator(Main mainFrame)(Code) creates the KeYMediator with a reference to the application's main frame and the current proof settings Method Detail addAutoModeListener public void addAutoModeListener(AutoModeListener listener)(Code) addGUIListener public void addGUIListener(GUIListener listener)(Code) adds a listener to GUI events Parameters:   listener - the GUIListener to be added addKeYSelectionListener public synchronized void addKeYSelectionListener(KeYSelectionListener listener)(Code) adds a listener to the KeYSelectionModel, so that the listener will be informed if the proof or node the user has selected changed Parameters:   listener - the KeYSelectionListener to add addRuleAppListener public void addRuleAppListener(RuleAppListener listener)(Code) applyInteractive public void applyInteractive(RuleApp app, Goal goal)(Code) Apply a RuleApp and continue with update simplification or strategy application according to current settings. Parameters:   app - Parameters:   goal - autoMode public boolean autoMode()(Code) changeNode public void changeNode(Node n)(Code) choice_ns public Namespace choice_ns()(Code) returns the choice namespace the choice namespace closedAGoal public void closedAGoal()(Code) ensureProofLoaded public boolean ensureProofLoaded()(Code) ensureProofLoadedSilent public boolean ensureProofLoadedSilent()(Code) fireModalDialogClosed public synchronized void fireModalDialogClosed(GUIEvent e)(Code) fires that a GUI component that has asked for modal access has been closed, so views can be enabled again fireModalDialogOpened public synchronized void fireModalDialogOpened(GUIEvent e)(Code) fires the request of a GUI component for modal access this can be used to disable all views even if the GUI component has no built in modal support fireShutDown public synchronized void fireShutDown(GUIEvent e)(Code) Fires the shut down event. freeModalAccess public synchronized void freeModalAccess(Object src)(Code) called if no more modal access is needed Parameters:   src - Object that is the asking component func_ns public Namespace func_ns()(Code) returns the function namespace the function namespace generateTestCaseForSelectedNode public void generateTestCaseForSelectedNode()(Code) getAutomaticApplicationTimeout public long getAutomaticApplicationTimeout()(Code) besides the number of rule applications it is possible to define a timeout after which rule application shall be terminated the time in ms after which automatic rule application stops getBuiltInRule public ListOfBuiltInRule getBuiltInRule(PosInOccurrence pos)(Code) collects all built-in rules a list of all applicable built-in rules getBuiltInRuleApplications public SetOfRuleApp getBuiltInRuleApplications(String name, PosInOccurrence pos)(Code) collects all applications of a rule given by its name at a give position in the sequent Parameters:   name - the name of the BuiltInRule for which applications are collected. Parameters:   pos - the position in the sequent where the BuiltInRule should be applieda SetOfRuleApp with all possible applications of the rule getExceptionHandler public KeYExceptionHandler getExceptionHandler()(Code) getFindTaclet public ListOfTacletApp getFindTaclet(PosInSequent pos)(Code) collects all applicable FindTaclets of the current goal (called by the SequentViewer) a list of Taclets with all applicable FindTaclets getInteractiveProver public InteractiveProver getInteractiveProver()(Code) Get the interactive prover. getJavaInfo public JavaInfo getJavaInfo()(Code) returns the JavaInfo with the java type information getMaxAutomaticSteps public int getMaxAutomaticSteps()(Code) returns the maximum number of rule applications allowed in automatic mode the maximum number of rule applications allowed inautomatic mode getMetavariableDeliverer public MetavariableDeliverer getMetavariableDeliverer()(Code) Deliverer of new metavariables (with unique names) getNoFindTaclet public ListOfTacletApp getNoFindTaclet()(Code) collects all applicable NoFindTaclets of the current goal (called by the SequentViewer) a list of Taclets with all applicable NoFindTaclets getNotationInfo public NotationInfo getNotationInfo()(Code) returns the used NotationInfo the used NotationInfo getNrGoalsClosedByAutoMode public int getNrGoalsClosedByAutoMode()(Code) getProfile public Profile getProfile()(Code) return the chosen profile getProof public Proof getProof()(Code) getProverTaskListener public ProverTaskListener getProverTaskListener()(Code) getReuseListener public ReuseListener getReuseListener()(Code) getRewriteTaclet public ListOfTacletApp getRewriteTaclet(PosInSequent pos)(Code) collects all applicable RewriteTaclets of the current goal (called by the SequentViewer) a list of Taclets with all applicable RewriteTaclets getSelectedGoal public Goal getSelectedGoal()(Code) returns the current selected goal the current selected goal getSelectedNode public Node getSelectedNode()(Code) returns the current selected node the current selected node getSelectedProof public Proof getSelectedProof()(Code) returns the current selected proof the current selected proof getSelectionModel public KeYSelectionModel getSelectionModel()(Code) returns the current selected goal the current selected goal getServices public Services getServices()(Code) returns the Services with the java service classes getTacletApplications public SetOfTacletApp getTacletApplications(Goal g, String name, PosInOccurrence p)(Code) getTacletApplications public SetOfTacletApp getTacletApplications(Goal goal, String name, PosInOccurrence pos, TacletFilter filter)(Code) getUserConstraint public ConstraintTableModel getUserConstraint()(Code) returns the user constraint (table model) the user constraint goalChosen public void goalChosen(Goal goal)(Code) sets the current goal Parameters:   goal - the Goal being displayed in the view of the sequent heur_ns public Namespace heur_ns()(Code) returns the heuristics namespace the heuristics namespace indicateNoReuse public void indicateNoReuse()(Code) indicateReuse public void indicateReuse(ReusePoint p)(Code) invokeAndWait public static void invokeAndWait(Runnable runner)(Code) mainFrame public JFrame mainFrame()(Code) returns the main frame the main frame mark public void mark(Node n)(Code) markPersistent public void markPersistent(Node n)(Code) namespaces public NamespaceSet namespaces()(Code) returns the namespace set the namespace set nonGoalNodeChosen public void nonGoalNodeChosen(Node node)(Code) notifies that a node that is not a goal has been chosen Parameters:   node - the node being displayed in the view of the sequent notify public void notify(NotificationEvent event)(Code) takes a notification event and informs the notification manager Parameters:   event - the NotificationEvent popupInformationMessage public void popupInformationMessage(Object message, String title)(Code) popupInformationMessage public void popupInformationMessage(Object message, String title, boolean modal)(Code) Brings up a dialog displaying a message. Parameters:   modal - whether or not the message should be displayed in a modal dialog. popupWarning public void popupWarning(Object message, String title)(Code) progVar_ns public Namespace progVar_ns()(Code) returns the program variable namespace the program variable namespace pv_ns public Namespace pv_ns()(Code) returns the prog var namespace the prog var namespace removeAutoModeListener public void removeAutoModeListener(AutoModeListener listener)(Code) removeGUIListener public void removeGUIListener(GUIListener listener)(Code) adds a listener to GUI events Parameters:   listener - the GUIListener to be added removeKeYSelectionListener public synchronized void removeKeYSelectionListener(KeYSelectionListener listener)(Code) removes a listener from the KeYSelectionModel Parameters:   listener - the KeYSelectionListener to be removed removeRuleAppListener public void removeRuleAppListener(RuleAppListener listener)(Code) requestModalAccess public synchronized void requestModalAccess(Object src)(Code) called to ask for modal access Parameters:   src - Object that is the asking component resetNrGoalsClosedByHeuristics public void resetNrGoalsClosedByHeuristics()(Code) reuseInProgress public boolean reuseInProgress()(Code) selectedBuiltInRule public void selectedBuiltInRule(BuiltInRule rule, PosInOccurrence pos)(Code) selected rule to apply Parameters:   rule - the selected built-in rule Parameters:   pos - the PosInSequent describes the position where to apply therule selectedTaclet public void selectedTaclet(TacletApp tacletApp, PosInSequent pos)(Code) selected rule to apply; opens a dialog Parameters:   tacletApp - the TacletApp which has been selected Parameters:   pos - the PosInSequent describes the position where to apply the rule selectedTaclet public boolean selectedTaclet(Taclet taclet, Goal goal, PosInOccurrence pos)(Code) selectedUseMethodContractRule public boolean selectedUseMethodContractRule(MethodContractRuleApp app)(Code) selected rule to apply Parameters:   rule - the selected built-in rule Parameters:   pos - the PosInSequent describes the position where to apply therule setAutomaticApplicationTimeout public void setAutomaticApplicationTimeout(long timeout)(Code) sets the time out after which automatic rule application stops Parameters:   timeout - a long specifying the timeout time in ms setBack public void setBack()(Code) Undo. author:    VK setBack public void setBack(Node node)(Code) setBack public void setBack(Goal goal)(Code) setCenter public static void setCenter(Component comp, Component parent)(Code) Center a component within a parental component. Parameters:   comp - the component to be centered. Parameters:   parent - center relative to what. null to center relative to screen. See Also:   KeYMediator.setCenter(Component) setCenter public static void setCenter(Component comp)(Code) Center a component on the screen. Parameters:   comp - the component to be centered relative to the screen.It must already have its final size set. setContinuousReuse public void setContinuousReuse(boolean b)(Code) setInteractive public void setInteractive(boolean b)(Code) Switches interactive mode on or off. Parameters:   b - true iff interactive mode is to be turned on setMaxAutomaticSteps public void setMaxAutomaticSteps(int steps)(Code) sets the maximum number of rule applications allowed in automatic mode Parameters:   steps - an int setting the limit setProof public void setProof(Proof p)(Code) initializes proof (this is Swing thread-safe) setResumeAutoMode public void setResumeAutoMode(boolean b)(Code) setSimplifier public void setSimplifier(UpdateSimplifier s)(Code) sets the simultaneous update simplifier setStupidMode public void setStupidMode(boolean b)(Code) showPreImage public void showPreImage()(Code) showReuseState public void showReuseState()(Code) sort_ns public Namespace sort_ns()(Code) returns the sort namespace the sort namespace startAutoMode public void startAutoMode()(Code) Start automatic application of rules on open goals. startAutoMode public void startAutoMode(ListOfGoal goals)(Code) Start automatic application of rules on specified goals. Parameters:   goals - startInterface public void startInterface(boolean fullStop)(Code) stopAutoMode public void stopAutoMode()(Code) Stop automatic application of rules. stopInterface public void stopInterface(boolean fullStop)(Code) stupidMode public boolean stupidMode()(Code) simplified user interface? testCaseConfirmation public void testCaseConfirmation(String path)(Code) testCaseConfirmation public void testCaseConfirmation(String path, int coverage)(Code) var_ns public Namespace var_ns()(Code) returns the variable namespace the variable namespace visualizeProof public ProofVisualization visualizeProof()(Code) Methods inherited from java.lang.Object protected Object clone() throws CloneNotSupportedException(Code)(Java Doc) public boolean equals(Object o)(Code)(Java Doc) protected void finalize() throws Throwable(Code)(Java Doc) final native public Class getClass()(Code)(Java Doc) public int hashCode()(Code)(Java Doc) final public void notify() throws IllegalMonitorStateException(Code)(Java Doc) final public void notifyAll() throws IllegalMonitorStateException(Code)(Java Doc) public String toString()(Code)(Java Doc) final public void wait() throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc) final public void wait(long ms) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc) final public void wait(long ms, int ns) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)