CPP/CSharp/Java/Javascript: Use concat in XMLParent.allCharactersString().

This commit is contained in:
Anders Schack-Mulligen 2018-09-26 15:47:21 +02:00
Родитель 26c1397216
Коммит 9198f5b9bd
4 изменённых файлов: 16 добавлений и 16 удалений

Просмотреть файл

@ -67,9 +67,12 @@ class XMLParent extends @xmlparent {
} }
/** /**
* DEPRECATED: Internal.
*
* Append the character sequences of this XML parent from left to right, separated by a space, * Append the character sequences of this XML parent from left to right, separated by a space,
* up to a specified (zero-based) index. * up to a specified (zero-based) index.
*/ */
deprecated
string charsSetUpTo(int n) { string charsSetUpTo(int n) {
(n = 0 and xmlChars(_,result,this,0,_,_)) or (n = 0 and xmlChars(_,result,this,0,_,_)) or
(n > 0 and exists(string chars | xmlChars(_,chars,this,n,_,_) | (n > 0 and exists(string chars | xmlChars(_,chars,this,n,_,_) |
@ -78,10 +81,7 @@ class XMLParent extends @xmlparent {
/** Append all the character sequences of this XML parent from left to right, separated by a space. */ /** Append all the character sequences of this XML parent from left to right, separated by a space. */
string allCharactersString() { string allCharactersString() {
exists(int n | n = this.getNumberOfCharacterSets() | result = concat(string chars, int pos | xmlChars(_, chars, this, pos, _, _) | chars, " " order by pos)
(n = 0 and result = "") or
(n > 0 and result = this.charsSetUpTo(n-1))
)
} }
/** Gets the text value contained in this XML parent. */ /** Gets the text value contained in this XML parent. */

Просмотреть файл

@ -79,9 +79,12 @@ class XMLParent extends @xmlparent {
} }
/** /**
* DEPRECATED: Internal.
*
* Append the character sequences of this XML parent from left to right, separated by a space, * Append the character sequences of this XML parent from left to right, separated by a space,
* up to a specified (zero-based) index. * up to a specified (zero-based) index.
*/ */
deprecated
string charsSetUpTo(int n) { string charsSetUpTo(int n) {
(n = 0 and xmlChars(_,result,this,0,_,_)) or (n = 0 and xmlChars(_,result,this,0,_,_)) or
(n > 0 and exists(string chars | xmlChars(_,chars,this,n,_,_) | (n > 0 and exists(string chars | xmlChars(_,chars,this,n,_,_) |
@ -90,10 +93,7 @@ class XMLParent extends @xmlparent {
/** Append all the character sequences of this XML parent from left to right, separated by a space. */ /** Append all the character sequences of this XML parent from left to right, separated by a space. */
string allCharactersString() { string allCharactersString() {
exists(int n | n = this.getNumberOfCharacterSets() | result = concat(string chars, int pos | xmlChars(_, chars, this, pos, _, _) | chars, " " order by pos)
(n = 0 and result = "") or
(n > 0 and result = this.charsSetUpTo(n-1))
)
} }
/** Gets the text value contained in this XML parent. */ /** Gets the text value contained in this XML parent. */

Просмотреть файл

@ -70,9 +70,12 @@ class XMLParent extends @xmlparent {
} }
/** /**
* DEPRECATED: Internal.
*
* Append the character sequences of this XML parent from left to right, separated by a space, * Append the character sequences of this XML parent from left to right, separated by a space,
* up to a specified (zero-based) index. * up to a specified (zero-based) index.
*/ */
deprecated
string charsSetUpTo(int n) { string charsSetUpTo(int n) {
n = 0 and xmlChars(_,result,this,0,_,_) n = 0 and xmlChars(_,result,this,0,_,_)
or or
@ -84,10 +87,7 @@ class XMLParent extends @xmlparent {
/** Append all the character sequences of this XML parent from left to right, separated by a space. */ /** Append all the character sequences of this XML parent from left to right, separated by a space. */
string allCharactersString() { string allCharactersString() {
exists(int n | n = this.getNumberOfCharacterSets() | result = concat(string chars, int pos | xmlChars(_, chars, this, pos, _, _) | chars, " " order by pos)
(n = 0 and result = "") or
(n > 0 and result = this.charsSetUpTo(n-1))
)
} }
/** Gets the text value contained in this XML parent. */ /** Gets the text value contained in this XML parent. */

Просмотреть файл

@ -70,9 +70,12 @@ class XMLParent extends @xmlparent {
} }
/** /**
* DEPRECATED: Internal.
*
* Append the character sequences of this XML parent from left to right, separated by a space, * Append the character sequences of this XML parent from left to right, separated by a space,
* up to a specified (zero-based) index. * up to a specified (zero-based) index.
*/ */
deprecated
string charsSetUpTo(int n) { string charsSetUpTo(int n) {
(n = 0 and xmlChars(_,result,this,0,_,_)) or (n = 0 and xmlChars(_,result,this,0,_,_)) or
(n > 0 and exists(string chars | xmlChars(_,chars,this,n,_,_) | (n > 0 and exists(string chars | xmlChars(_,chars,this,n,_,_) |
@ -81,10 +84,7 @@ class XMLParent extends @xmlparent {
/** Append all the character sequences of this XML parent from left to right, separated by a space. */ /** Append all the character sequences of this XML parent from left to right, separated by a space. */
string allCharactersString() { string allCharactersString() {
exists(int n | n = this.getNumberOfCharacterSets() | result = concat(string chars, int pos | xmlChars(_, chars, this, pos, _, _) | chars, " " order by pos)
(n = 0 and result = "") or
(n > 0 and result = this.charsSetUpTo(n-1))
)
} }
/** Gets the text value contained in this XML parent. */ /** Gets the text value contained in this XML parent. */