public class TermNavigator
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
static TermNavigator |
get(Term term)
returns a pooled
TermNavigator or a new one if the TERM_NAVIGATOR_POOL is currently empty
The used TermNavigator have to be explicitly released by the user via release() |
Term |
getCurrentSubterm() |
void |
gotoNext() |
void |
gotoNextSibling() |
boolean |
hasNext() |
boolean |
hasNextSibling() |
void |
release() |
public static TermNavigator get(Term term)
TermNavigator
or a new one if the TERM_NAVIGATOR_POOL is currently empty
The used TermNavigator have to be explicitly released by the user via release()
TermNavigator
or a new one if the TERM_NAVIGATOR_POOL is currently emptypublic boolean hasNext()
public boolean hasNextSibling()
public Term getCurrentSubterm()
public void gotoNext()
public void gotoNextSibling()
public void release()
Copyright © 2003-2019 The KeY-Project.