From 7f765692568c6b763e9f040a5b1ed110dc094bc2 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Fri, 19 Jul 2024 13:43:47 +0200 Subject: [PATCH] doc: Add docstring to some attributes Without docstrings, users will see the generic documentation of `declModifiers`. --- ProofWidgets/Cancellable.lean | 4 ++++ ProofWidgets/Presentation/Expr.lean | 1 + 2 files changed, 5 insertions(+) diff --git a/ProofWidgets/Cancellable.lean b/ProofWidgets/Cancellable.lean index b2da0ba..013c87d 100644 --- 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 index 7dd1c22..17c1e55 100644 --- 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`."