From 0bc66dcdc5dfd4477c6daf5f10ca8e34f3db174d Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 26 Jan 2024 18:01:23 +0100
Subject: [PATCH] add doc comments

---
 src/Lean/Data/Position.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index 23bcbb6a5f67..1a29853624e1 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -29,9 +29,16 @@ instance : ToExpr Position where
 
 end Position
 
+/-- Content of a file together with precalculated positions of newlines. -/
 structure FileMap where
+  /-- The content of the file. -/
   source    : String
+  /-- The positions of newline characters.
+  The first entry is always `0` and the last always the index of the last character.
+  In particular, if the last character is a newline, that index will appear twice. -/
   positions : Array String.Pos
+  /-- The line indices. Has the same length as `positions` and is always of the form
+  `[1, 2, …, n-1, n-1]`. -/
   lines     : Array Nat
   deriving Inhabited