/// <summary>
		/// Rebuild the tree, in O(n).
		/// </summary>
		public void RebuildDocument()
		{
			foreach (CollapsedLineSection s in GetAllCollapsedSections()) {
				s.Start = null;
				s.End = null;
			}
			
			HeightTreeNode[] nodes = new HeightTreeNode[document.LineCount];
			int lineNumber = 0;
			foreach (DocumentLine ls in document.Lines) {
				nodes[lineNumber++] = new HeightTreeNode(ls, DefaultLineHeight);
			}
			Debug.Assert(nodes.Length > 0);
			// now build the corresponding balanced tree
			int height = DocumentLineTree.GetTreeHeight(nodes.Length);
			Debug.WriteLine("HeightTree will have height: " + height);
			root = BuildTree(nodes, 0, nodes.Length, height);
			root.color = BLACK;
			#if DEBUG
			CheckProperties();
			#endif
		}

		void CheckProperties(HeightTreeNode node)
		{
			int totalCount = 1;
			double totalHeight = node.lineNode.TotalHeight;
			if (node.lineNode.IsDirectlyCollapsed)
				Debug.Assert(node.lineNode.collapsedSections.Count > 0);
			if (node.left != null) {
				CheckProperties(node.left);
				totalCount += node.left.totalCount;
				totalHeight += node.left.totalHeight;
				
				CheckAllContainedIn(node.left.collapsedSections, node.lineNode.collapsedSections);
			}
			if (node.right != null) {
				CheckProperties(node.right);
				totalCount += node.right.totalCount;
				totalHeight += node.right.totalHeight;
				
				CheckAllContainedIn(node.right.collapsedSections, node.lineNode.collapsedSections);
			}
			if (node.left != null && node.right != null) {
				if (node.left.collapsedSections != null && node.right.collapsedSections != null) {
					var intersection = System.Linq.Enumerable.Intersect(node.left.collapsedSections, node.right.collapsedSections);
					Debug.Assert(System.Linq.Enumerable.Count(intersection) == 0);
				}
			}
			if (node.IsDirectlyCollapsed) {
				Debug.Assert(node.collapsedSections.Count > 0);
				totalHeight = 0;
			}
			Debug.Assert(node.totalCount == totalCount);
			Debug.Assert(node.totalHeight.IsClose(totalHeight));
		}

		static bool GetColor(HeightTreeNode node)
		{
			return node != null ? node.color : BLACK;
		}

		static HeightTreeNode Sibling(HeightTreeNode node)
		{
			if (node == node.parent.left)
				return node.parent.right;
			else
				return node.parent.left;
		}

		void ReplaceNode(HeightTreeNode replacedNode, HeightTreeNode newNode)
		{
			if (replacedNode.parent == null) {
				Debug.Assert(replacedNode == root);
				root = newNode;
			} else {
				if (replacedNode.parent.left == replacedNode)
					replacedNode.parent.left = newNode;
				else
					replacedNode.parent.right = newNode;
			}
			if (newNode != null) {
				newNode.parent = replacedNode.parent;
			}
			replacedNode.parent = null;
		}

		void RemoveNode(HeightTreeNode removedNode)
		{
			if (removedNode.left != null && removedNode.right != null) {
				// replace removedNode with it's in-order successor
				
				HeightTreeNode leftMost = removedNode.right.LeftMost;
				HeightTreeNode parentOfLeftMost = leftMost.parent;
				RemoveNode(leftMost); // remove leftMost from its current location
				
				BeforeNodeReplace(removedNode, leftMost, parentOfLeftMost);
				// and overwrite the removedNode with it
				ReplaceNode(removedNode, leftMost);
				leftMost.left = removedNode.left;
				if (leftMost.left != null) leftMost.left.parent = leftMost;
				leftMost.right = removedNode.right;
				if (leftMost.right != null) leftMost.right.parent = leftMost;
				leftMost.color = removedNode.color;
				
				UpdateAfterChildrenChange(leftMost);
				if (leftMost.parent != null) UpdateAfterChildrenChange(leftMost.parent);
				return;
			}
			
			// now either removedNode.left or removedNode.right is null
			// get the remaining child
			HeightTreeNode parentNode = removedNode.parent;
			HeightTreeNode childNode = removedNode.left ?? removedNode.right;
			BeforeNodeRemove(removedNode);
			ReplaceNode(removedNode, childNode);
			if (parentNode != null) UpdateAfterChildrenChange(parentNode);
			if (removedNode.color == BLACK) {
				if (childNode != null && childNode.color == RED) {
					childNode.color = BLACK;
				} else {
					FixTreeOnDelete(childNode, parentNode);
				}
			}
		}

		void InsertAsRight(HeightTreeNode parentNode, HeightTreeNode newNode)
		{
			Debug.Assert(parentNode.right == null);
			parentNode.right = newNode;
			newNode.parent = parentNode;
			newNode.color = RED;
			UpdateAfterChildrenChange(parentNode);
			FixTreeOnInsert(newNode);
		}

		static void UpdateAugmentedData(HeightTreeNode node, UpdateAfterChildrenChangeRecursionMode mode)
		{
			int totalCount = 1;
			double totalHeight = node.lineNode.TotalHeight;
			if (node.left != null) {
				totalCount += node.left.totalCount;
				totalHeight += node.left.totalHeight;
			}
			if (node.right != null) {
				totalCount += node.right.totalCount;
				totalHeight += node.right.totalHeight;
			}
			if (node.IsDirectlyCollapsed)
				totalHeight = 0;
			if (totalCount != node.totalCount
			    || !totalHeight.IsClose(node.totalHeight)
			    || mode == UpdateAfterChildrenChangeRecursionMode.WholeBranch)
			{
				node.totalCount = totalCount;
				node.totalHeight = totalHeight;
				if (node.parent != null && mode != UpdateAfterChildrenChangeRecursionMode.None)
					UpdateAugmentedData(node.parent, mode);
			}
		}

		static void UpdateAfterChildrenChange(HeightTreeNode node)
		{
			UpdateAugmentedData(node, UpdateAfterChildrenChangeRecursionMode.IfRequired);
		}

		HeightTreeNode InsertAfter(HeightTreeNode node, DocumentLine newLine)
		{
			HeightTreeNode newNode = new HeightTreeNode(newLine, defaultLineHeight);
			if (node.right == null) {
				if (node.lineNode.collapsedSections != null) {
					// we are inserting directly after node - so copy all collapsedSections
					// that do not end at node.
					foreach (CollapsedLineSection cs in node.lineNode.collapsedSections) {
						if (cs.End != node.documentLine)
							newNode.AddDirectlyCollapsed(cs);
					}
				}
				InsertAsRight(node, newNode);
			} else {
				node = node.right.LeftMost;
				if (node.lineNode.collapsedSections != null) {
					// we are inserting directly before node - so copy all collapsedSections
					// that do not start at node.
					foreach (CollapsedLineSection cs in node.lineNode.collapsedSections) {
						if (cs.Start != node.documentLine)
							newNode.AddDirectlyCollapsed(cs);
					}
				}
				InsertAsLeft(node, newNode);
			}
			return newNode;
		}

		/// <summary>
		/// build a tree from a list of nodes
		/// </summary>
		HeightTreeNode BuildTree(HeightTreeNode[] nodes, int start, int end, int subtreeHeight)
		{
			Debug.Assert(start <= end);
			if (start == end) {
				return null;
			}
			int middle = (start + end) / 2;
			HeightTreeNode node = nodes[middle];
			node.left = BuildTree(nodes, start, middle, subtreeHeight - 1);
			node.right = BuildTree(nodes, middle + 1, end, subtreeHeight - 1);
			if (node.left != null) node.left.parent = node;
			if (node.right != null) node.right.parent = node;
			if (subtreeHeight == 1)
				node.color = RED;
			UpdateAugmentedData(node, UpdateAfterChildrenChangeRecursionMode.None);
			return node;
		}

		static void AddRemoveCollapsedSectionDown(CollapsedLineSection section, HeightTreeNode node, int sectionLength, bool add)
		{
			while (true) {
				if (node.left != null) {
					if (node.left.totalCount < sectionLength) {
						// mark left subtree
						if (add)
							node.left.AddDirectlyCollapsed(section);
						else
							node.left.RemoveDirectlyCollapsed(section);
						sectionLength -= node.left.totalCount;
					} else {
						// mark only inside the left subtree
						node = node.left;
						Debug.Assert(node != null);
						continue;
					}
				}
				if (add)
					node.lineNode.AddDirectlyCollapsed(section);
				else
					node.lineNode.RemoveDirectlyCollapsed(section);
				sectionLength -= 1;
				if (sectionLength == 0) {
					// done!
					Debug.Assert(node.documentLine == section.End);
					break;
				}
				// mark inside right subtree:
				node = node.right;
				Debug.Assert(node != null);
			}
		}

		static bool GetIsCollapedFromNode(HeightTreeNode node)
		{
			while (node != null) {
				if (node.IsDirectlyCollapsed)
					return true;
				node = node.parent;
			}
			return false;
		}

		/*
		1. A node is either red or black.
		2. The root is black.
		3. All leaves are black. (The leaves are the NIL children.)
		4. Both children of every red node are black. (So every red node must have a black parent.)
		5. Every simple path from a node to a descendant leaf contains the same number of black nodes. (Not counting the leaf node.)
		 */
		void CheckNodeProperties(HeightTreeNode node, HeightTreeNode parentNode, bool parentColor, int blackCount, ref int expectedBlackCount)
		{
			if (node == null) return;
			
			Debug.Assert(node.parent == parentNode);
			
			if (parentColor == RED) {
				Debug.Assert(node.color == BLACK);
			}
			if (node.color == BLACK) {
				blackCount++;
			}
			if (node.left == null && node.right == null) {
				// node is a leaf node:
				if (expectedBlackCount == -1)
					expectedBlackCount = blackCount;
				else
					Debug.Assert(expectedBlackCount == blackCount);
			}
			CheckNodeProperties(node.left, node, node.color, blackCount, ref expectedBlackCount);
			CheckNodeProperties(node.right, node, node.color, blackCount, ref expectedBlackCount);
		}

		static void AppendTreeToString(HeightTreeNode node, StringBuilder b, int indent)
		{
			if (node.color == RED)
				b.Append("RED   ");
			else
				b.Append("BLACK ");
			b.AppendLine(node.ToString());
			indent += 2;
			if (node.left != null) {
				b.Append(' ', indent);
				b.Append("L: ");
				AppendTreeToString(node.left, b, indent);
			}
			if (node.right != null) {
				b.Append(' ', indent);
				b.Append("R: ");
				AppendTreeToString(node.right, b, indent);
			}
		}

		void UpdateAfterRotateRight(HeightTreeNode node)
		{
			// node = old parent
			// node.parent = pivot, new parent
			var collapsedP = node.parent.collapsedSections;
			var collapsedQ = node.collapsedSections;
			// move collapsedSections from old parent to new parent
			node.parent.collapsedSections = collapsedQ;
			node.collapsedSections = null;
			// split the collapsedSections from the new parent into its old children:
			if (collapsedP != null) {
				foreach (CollapsedLineSection cs in collapsedP) {
					if (node.parent.left != null)
						node.parent.left.AddDirectlyCollapsed(cs);
					node.parent.lineNode.AddDirectlyCollapsed(cs);
					if (node.left != null)
						node.left.AddDirectlyCollapsed(cs);
				}
			}
			MergeCollapsedSectionsIfPossible(node);
			
			UpdateAfterChildrenChange(node);
			
			// not required: rotations only happen on insertions/deletions
			// -> totalCount changes -> the parent is always updated
			//UpdateAfterChildrenChange(node.parent);
		}

		void FixTreeOnInsert(HeightTreeNode node)
		{
			Debug.Assert(node != null);
			Debug.Assert(node.color == RED);
			Debug.Assert(node.left == null || node.left.color == BLACK);
			Debug.Assert(node.right == null || node.right.color == BLACK);
			
			HeightTreeNode parentNode = node.parent;
			if (parentNode == null) {
				// we inserted in the root -> the node must be black
				// since this is a root node, making the node black increments the number of black nodes
				// on all paths by one, so it is still the same for all paths.
				node.color = BLACK;
				return;
			}
			if (parentNode.color == BLACK) {
				// if the parent node where we inserted was black, our red node is placed correctly.
				// since we inserted a red node, the number of black nodes on each path is unchanged
				// -> the tree is still balanced
				return;
			}
			// parentNode is red, so there is a conflict here!
			
			// because the root is black, parentNode is not the root -> there is a grandparent node
			HeightTreeNode grandparentNode = parentNode.parent;
			HeightTreeNode uncleNode = Sibling(parentNode);
			if (uncleNode != null && uncleNode.color == RED) {
				parentNode.color = BLACK;
				uncleNode.color = BLACK;
				grandparentNode.color = RED;
				FixTreeOnInsert(grandparentNode);
				return;
			}
			// now we know: parent is red but uncle is black
			// First rotation:
			if (node == parentNode.right && parentNode == grandparentNode.left) {
				RotateLeft(parentNode);
				node = node.left;
			} else if (node == parentNode.left && parentNode == grandparentNode.right) {
				RotateRight(parentNode);
				node = node.right;
			}
			// because node might have changed, reassign variables:
			parentNode = node.parent;
			grandparentNode = parentNode.parent;
			
			// Now recolor a bit:
			parentNode.color = BLACK;
			grandparentNode.color = RED;
			// Second rotation:
			if (node == parentNode.left && parentNode == grandparentNode.left) {
				RotateRight(grandparentNode);
			} else {
				// because of the first rotation, this is guaranteed:
				Debug.Assert(node == parentNode.right && parentNode == grandparentNode.right);
				RotateLeft(grandparentNode);
			}
		}

		// node removal:
		// a node in the middle of the tree is removed as following:
		//  its successor is removed
		//  it is replaced with its successor
		
		void BeforeNodeRemove(HeightTreeNode removedNode)
		{
			Debug.Assert(removedNode.left == null || removedNode.right == null);
			
			var collapsed = removedNode.collapsedSections;
			if (collapsed != null) {
				HeightTreeNode childNode = removedNode.left ?? removedNode.right;
				if (childNode != null) {
					foreach (CollapsedLineSection cs in collapsed)
						childNode.AddDirectlyCollapsed(cs);
				}
			}
			if (removedNode.parent != null)
				MergeCollapsedSectionsIfPossible(removedNode.parent);
		}

		void FixTreeOnDelete(HeightTreeNode node, HeightTreeNode parentNode)
		{
			Debug.Assert(node == null || node.parent == parentNode);
			if (parentNode == null)
				return;
			
			// warning: node may be null
			HeightTreeNode sibling = Sibling(node, parentNode);
			if (sibling.color == RED) {
				parentNode.color = RED;
				sibling.color = BLACK;
				if (node == parentNode.left) {
					RotateLeft(parentNode);
				} else {
					RotateRight(parentNode);
				}
				
				sibling = Sibling(node, parentNode); // update value of sibling after rotation
			}
			
			if (parentNode.color == BLACK
			    && sibling.color == BLACK
			    && GetColor(sibling.left) == BLACK
			    && GetColor(sibling.right) == BLACK)
			{
				sibling.color = RED;
				FixTreeOnDelete(parentNode, parentNode.parent);
				return;
			}
			
			if (parentNode.color == RED
			    && sibling.color == BLACK
			    && GetColor(sibling.left) == BLACK
			    && GetColor(sibling.right) == BLACK)
			{
				sibling.color = RED;
				parentNode.color = BLACK;
				return;
			}
			
			if (node == parentNode.left &&
			    sibling.color == BLACK &&
			    GetColor(sibling.left) == RED &&
			    GetColor(sibling.right) == BLACK)
			{
				sibling.color = RED;
				sibling.left.color = BLACK;
				RotateRight(sibling);
			}
			else if (node == parentNode.right &&
			         sibling.color == BLACK &&
			         GetColor(sibling.right) == RED &&
			         GetColor(sibling.left) == BLACK)
			{
				sibling.color = RED;
				sibling.right.color = BLACK;
				RotateLeft(sibling);
			}
			sibling = Sibling(node, parentNode); // update value of sibling after rotation
			
			sibling.color = parentNode.color;
			parentNode.color = BLACK;
			if (node == parentNode.left) {
				if (sibling.right != null) {
					Debug.Assert(sibling.right.color == RED);
					sibling.right.color = BLACK;
				}
				RotateLeft(parentNode);
			} else {
				if (sibling.left != null) {
					Debug.Assert(sibling.left.color == RED);
					sibling.left.color = BLACK;
				}
				RotateRight(parentNode);
			}
		}

		void BeforeNodeReplace(HeightTreeNode removedNode, HeightTreeNode newNode, HeightTreeNode newNodeOldParent)
		{
			Debug.Assert(removedNode != null);
			Debug.Assert(newNode != null);
			while (newNodeOldParent != removedNode) {
				if (newNodeOldParent.collapsedSections != null) {
					foreach (CollapsedLineSection cs in newNodeOldParent.collapsedSections) {
						newNode.lineNode.AddDirectlyCollapsed(cs);
					}
				}
				newNodeOldParent = newNodeOldParent.parent;
			}
			if (newNode.collapsedSections != null) {
				foreach (CollapsedLineSection cs in newNode.collapsedSections) {
					newNode.lineNode.AddDirectlyCollapsed(cs);
				}
			}
			newNode.collapsedSections = removedNode.collapsedSections;
			MergeCollapsedSectionsIfPossible(newNode);
		}