001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.common;
017
018 import org.qedeq.kernel.se.base.list.Element;
019 import org.qedeq.kernel.se.common.ModuleContext;
020 import org.qedeq.kernel.se.dto.module.NodeVo;
021 import org.qedeq.kernel.se.visitor.QedeqNumbers;
022
023 /**
024 * Represents a node and its properties.
025 *
026 * @author Michael Meyling
027 */
028 public interface NodeBo {
029
030 /**
031 * Get parent the node is in.
032 *
033 * @return Parent module for this node.
034 */
035 public QedeqBo getParentQedeqBo();
036
037 /**
038 * Get numbers of node.
039 *
040 * @return Node numbers.
041 */
042 public QedeqNumbers getNumbers();
043
044 /**
045 * Get module context the node is within.
046 *
047 * @return The module context the node is within.
048 */
049 public ModuleContext getModuleContext();
050
051 /**
052 * Was this node checked successfully for formal correctness? This means checking the formal
053 * syntax of the node formulas. This includes all formulas. LaTeX correctness doesn't play any
054 * role. Nodes without formal formulas return always <code>true</code>.
055 *
056 * @return <code>true</code> if the check was successful.
057 */
058 public boolean isWellFormed();
059
060 /**
061 * Was this node checked unsuccessfully for formal correctness? This means checking the formal
062 * syntax of the node formulas. This includes all formulas. LaTeX correctness doesn't play any
063 * role. Nodes without formal formulas return always <code>false</code>.
064 *
065 * @return <code>true</code> if the check was not successful.
066 */
067 public boolean isNotWellFormed();
068
069 /**
070 * This means that at least one formal proof was successfully checked for correctness.
071 * For non propositions we always get <code>true</code>.
072 *
073 * @return <code>true</code> if the check was successful.
074 */
075 public boolean isProved();
076
077 /**
078 * This means that at least not even one formal proof could be successfully checked for
079 * correctness.
080 * For non propositions we always get <code>false</code>.
081 *
082 * @return <code>true</code> if the check was not successful.
083 */
084 public boolean isNotProved();
085
086 /**
087 * Has this node a formula?
088 *
089 * @return Formula.
090 */
091 public boolean hasFormula();
092
093 /**
094 * Get formula of node. Can only be not <code>null</code> if this node is an Axiom,
095 * PredicateDefinition, FunctionDefinition or Proposition.
096 *
097 * @return Node formula.
098 */
099 public Element getFormula();
100
101 /**
102 * Get node.
103 *
104 * @return Node.
105 */
106 public NodeVo getNodeVo();
107
108 }
|