/* 
    P/P   *  Method: com.dmdirc.addons.ui_swing.textpane.LinePosition__static_init
          */
     1  /*
     2   * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
     3   * 
     4   * Permission is hereby granted, free of charge, to any person obtaining a copy
     5   * of this software and associated documentation files (the "Software"), to deal
     6   * in the Software without restriction, including without limitation the rights
     7   * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
     8   * copies of the Software, and to permit persons to whom the Software is
     9   * furnished to do so, subject to the following conditions:
    10   * 
    11   * The above copyright notice and this permission notice shall be included in
    12   * all copies or substantial portions of the Software.
    13   * 
    14   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
    15   * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
    16   * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
    17   * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
    18   * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
    19   * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
    20   * SOFTWARE.
    21   */
    22  
    23  package com.dmdirc.addons.ui_swing.textpane;
    24  
    25  /**
    26   * Holds information about a range of text.
    27   */
    28  public class LinePosition {
    29  
    30      /** Starting line. */
    31      private int startLine;
    32      /** Ending line. */
    33      private int endLine;
    34      /** Starting position. */
    35      private int startPos;
    36      /** Ending position. */
    37      private int endPos;
    38  
    39      /**
    40       * Constructs a new line position.
    41       * 
    42       * @param startLine Starting line
    43       * @param endLine Ending line
    44       * @param startPos Starting position
    45       * @param endPos Ending position
    46       */
    47      public LinePosition(final int startLine, final int startPos,
                     /* 
    P/P               *  Method: void com.dmdirc.addons.ui_swing.textpane.LinePosition(int, int, int, int)
                      * 
                      *  Postconditions:
                      *    this.endLine == endLine
                      *    init'ed(this.endLine)
                      *    this.endPos == endPos
                      *    init'ed(this.endPos)
                      *    this.startLine == startLine
                      *    init'ed(this.startLine)
                      *    this.startPos == startPos
                      *    init'ed(this.startPos)
                      */
    48              final int endLine, final int endPos) {
    49          this.startLine = startLine;
    50          this.endLine = endLine;
    51          this.startPos = startPos;
    52          this.endPos = endPos;
    53      }
    54  
    55      /**
    56       * Constructs a new line position.
    57       *
    58       * @param position Position to create position from
    59       */
             /* 
    P/P       *  Method: void com.dmdirc.addons.ui_swing.textpane.LinePosition(LinePosition)
              * 
              *  Preconditions:
              *    position != null
              *    init'ed(position.endLine)
              *    init'ed(position.endPos)
              *    init'ed(position.startLine)
              *    init'ed(position.startPos)
              * 
              *  Postconditions:
              *    this.endLine == position.endLine
              *    init'ed(this.endLine)
              *    this.endPos == position.endPos
              *    init'ed(this.endPos)
              *    this.startLine == position.startLine
              *    init'ed(this.startLine)
              *    this.startPos == position.startPos
              *    init'ed(this.startPos)
              */
    60      public LinePosition(final LinePosition position) {
    61          this.startLine = position.getStartLine();
    62          this.endLine = position.getEndLine();
    63          this.startPos = position.getStartPos();
    64          this.endPos = position.getEndPos();
    65      }
    66  
    67      /**
    68       * Returns the end line for this position.
    69       * 
    70       * @return End line
    71       */
    72      public int getEndLine() {
                 /* 
    P/P           *  Method: int getEndLine()
                  * 
                  *  Preconditions:
                  *    init'ed(this.endLine)
                  * 
                  *  Postconditions:
                  *    return_value == this.endLine
                  *    init'ed(return_value)
                  */
    73          return endLine;
    74      }
    75  
    76      /**
    77       * Returns the end position for this position.
    78       * 
    79       * @return End position
    80       */
    81      public int getEndPos() {
                 /* 
    P/P           *  Method: int getEndPos()
                  * 
                  *  Preconditions:
                  *    init'ed(this.endPos)
                  * 
                  *  Postconditions:
                  *    return_value == this.endPos
                  *    init'ed(return_value)
                  */
    82          return endPos;
    83      }
    84  
    85      /**
    86       * Returns the start line for this position.
    87       * 
    88       * @return Start line
    89       */
    90      public int getStartLine() {
                 /* 
    P/P           *  Method: int getStartLine()
                  * 
                  *  Preconditions:
                  *    init'ed(this.startLine)
                  * 
                  *  Postconditions:
                  *    return_value == this.startLine
                  *    init'ed(return_value)
                  */
    91          return startLine;
    92      }
    93  
    94      /**
    95       * Returns the start position for this position.
    96       * 
    97       * @return Start position
    98       */
    99      public int getStartPos() {
                 /* 
    P/P           *  Method: int getStartPos()
                  * 
                  *  Preconditions:
                  *    init'ed(this.startPos)
                  * 
                  *  Postconditions:
                  *    return_value == this.startPos
                  *    init'ed(return_value)
                  */
   100          return startPos;
   101      }
   102      
   103      /**
   104       * Sets the positions end line.
   105       * 
   106       * @param endLine new end line
   107       */
   108      public void setEndLine(int endLine) {
                 /* 
    P/P           *  Method: void setEndLine(int)
                  * 
                  *  Postconditions:
                  *    this.endLine == endLine
                  *    init'ed(this.endLine)
                  */
   109          this.endLine = endLine;
   110      }
   111  
   112      /**
   113       * Sets the positions end line.
   114       * 
   115       * @param endPos new end line
   116       */
   117      public void setEndPos(int endPos) {
                 /* 
    P/P           *  Method: void setEndPos(int)
                  * 
                  *  Postconditions:
                  *    this.endPos == endPos
                  *    init'ed(this.endPos)
                  */
   118          this.endPos = endPos;
   119      }
   120  
   121      /**
   122       * Sets the positions start line.
   123       * 
   124       * @param startLine new start line
   125       */
   126      public void setStartLine(int startLine) {
                 /* 
    P/P           *  Method: void setStartLine(int)
                  * 
                  *  Postconditions:
                  *    this.startLine == startLine
                  *    init'ed(this.startLine)
                  */
   127          this.startLine = startLine;
   128      }
   129  
   130      /**
   131       * Sets the positions start position.
   132       * 
   133       * @param startPos new start position
   134       */
   135      public void setStartPos(int startPos) {
                 /* 
    P/P           *  Method: void setStartPos(int)
                  * 
                  *  Postconditions:
                  *    this.startPos == startPos
                  *    init'ed(this.startPos)
                  */
   136          this.startPos = startPos;
   137      }
   138      
   139      /** {@inheritDoc} */
   140      @Override
   141      public String toString() {
                 /* 
    P/P           *  Method: String toString()
                  * 
                  *  Preconditions:
                  *    init'ed(this.endLine)
                  *    init'ed(this.endPos)
                  *    init'ed(this.startLine)
                  *    init'ed(this.startPos)
                  * 
                  *  Postconditions:
                  *    java.lang.StringBuilder:toString(...)._tainted == 0
                  *    return_value == &java.lang.StringBuilder:toString(...)
                  */
   142          return "Position[" + startLine + ", " + startPos + ", " + endLine + ", " + endPos + "]";
   143      }
   144  }