From 3e785b658c0f2300801b59a81691b8e8b29b0292 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 24 Nov 2024 10:29:22 +1100 Subject: [PATCH 1/2] . --- ProofWidgets/Component/HtmlDisplay.lean | 4 +++- ProofWidgets/Presentation/Expr.lean | 15 --------------- 2 files changed, 3 insertions(+), 16 deletions(-) diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean index fcfd477..85e8eee 100644 --- a/ProofWidgets/Component/HtmlDisplay.lean +++ b/ProofWidgets/Component/HtmlDisplay.lean @@ -74,7 +74,9 @@ def elabHtmlCmd : CommandElab := fun /-- The `html!` tactic is deprecated and does nothing. If you have a use for it, please open an issue on https://github.com/leanprover-community/ProofWidgets4. -/ -@[deprecated] +@[deprecated "The `html!` tactic is deprecated and does nothing. If you have a use for it, \ + please open an issue on https://github.com/leanprover-community/ProofWidgets4." + (since := "2024-05-15")] syntax (name := htmlTac) "html! " term : tactic open Tactic in diff --git a/ProofWidgets/Presentation/Expr.lean b/ProofWidgets/Presentation/Expr.lean index 17c1e55..790ced6 100644 --- a/ProofWidgets/Presentation/Expr.lean +++ b/ProofWidgets/Presentation/Expr.lean @@ -81,21 +81,6 @@ structure GetExprPresentationParams where name : Name deriving RpcEncodable -@[server_rpc_method] -def getExprPresentation : GetExprPresentationParams → RequestM (RequestTask Html) - | { expr := ⟨expr⟩, name } => RequestM.asTask do - let ci := expr.ci - if !exprPresenters.hasTag ci.env name then - throw <| RequestError.invalidParams s!"The constant '{name}' is not an Expr presenter." - match evalExprPresenter ci.env ci.options name with - | .ok p => - expr.runMetaM p.present - | .error e => - throw <| RequestError.internalError s!"Failed to evaluate Expr presenter '{name}': {e}" - --- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/deprecation.20warning.20from.20ProofWidgets -attribute [deprecated] getExprPresentation - structure ExprPresentationProps where expr : WithRpcRef ExprWithCtx deriving RpcEncodable From 3cc4cd1a2495780516b1e0b59d63461ef90844da Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 23 Nov 2024 21:40:45 -0500 Subject: [PATCH 2/2] chore: remove deprecated `html!` tactic --- ProofWidgets/Component/HtmlDisplay.lean | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean index 85e8eee..e59c655 100644 --- a/ProofWidgets/Component/HtmlDisplay.lean +++ b/ProofWidgets/Component/HtmlDisplay.lean @@ -71,18 +71,6 @@ def elabHtmlCmd : CommandElab := fun stx | stx => throwError "Unexpected syntax {stx}." -/-- The `html!` tactic is deprecated and does nothing. -If you have a use for it, -please open an issue on https://github.com/leanprover-community/ProofWidgets4. -/ -@[deprecated "The `html!` tactic is deprecated and does nothing. If you have a use for it, \ - please open an issue on https://github.com/leanprover-community/ProofWidgets4." - (since := "2024-05-15")] -syntax (name := htmlTac) "html! " term : tactic - -open Tactic in -@[tactic htmlTac] -def elabHtmlTac : Tactic | _ => pure () - end HtmlCommand end ProofWidgets