From dca9278e09c38e883caa9b1a8c3f8600a4389040 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Aug 2021 13:45:36 -0700
Subject: [PATCH] feat: add `elabModuleDoc`

---
 src/Lean/Elab/BuiltinCommand.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 27dd560bc2..cf6c08e208 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -3,11 +3,19 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.DocString
 import Lean.Elab.Command
 import Lean.Elab.Open
 
 namespace Lean.Elab.Command
 
+@[builtinCommandElab moduleDoc] def elabModuleDoc : CommandElab := fun stx =>
+   match stx[1] with
+   | Syntax.atom _ val =>
+     let doc := val.extract 0 (val.bsize - 2)
+     modifyEnv fun env => addMainModuleDoc env doc
+   | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
+
 private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => { s with
     env    := s.env.registerNamespace newNamespace,