diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index 23bcbb6a5f..aba88c65ca 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 numbers associated with the `positions`.
+  Has the same length as `positions` and is always of the form `#[1, 2, …, n-1, n-1]`. -/
   lines     : Array Nat
   deriving Inhabited