Merge pull request #71 from PatrickMassot/pm_docstring

doc: Add docstring to some attributes
leanprover-community · Jul 19, 2024 · eaba628 · eaba628
2 parents d1b3320 + 7f76569
commit eaba628
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/ProofWidgets/Cancellable.lean b/ProofWidgets/Cancellable.lean
@@ -80,6 +80,10 @@ def checkRequest (rid : RequestId) : RequestM (RequestTask CheckRequestResponse)
 
 def cancellableSuffix : Name := `_cancellable
 
+/-- Like `server_rpc_method`, but requests for this method can be cancelled.
+The method should check for that using `IO.checkCanceled`.
+Cancellable methods are invoked differently from JavaScript:
+see `callCancellable` in `cancellable.ts`. -/
 initialize
   registerBuiltinAttribute {
     name := `server_rpc_method_cancellable

diff --git a/ProofWidgets/Presentation/Expr.lean b/ProofWidgets/Presentation/Expr.lean
@@ -14,6 +14,7 @@ structure ExprPresenter where
   layoutKind : LayoutKind := .block
   present : Expr → MetaM Html
 
+/-- Register an Expr presenter. It must have the type `ProofWidgets.ExprPresenter`. -/
 initialize exprPresenters : TagAttribute ←
   registerTagAttribute `expr_presenter
     "Register an Expr presenter. It must have the type `ProofWidgets.ExprPresenter`."