fix(tactic/doc_commands): do not construct json by hand (#4501)

Fixes three lines going over the 100 character limit.

The first one was a hand-rolled JSON serializer, I took the liberty to migrate it to the new `json` API.

src/tactic/doc_commands.lean

@@ -138,15 +138,18 @@ structure tactic_doc_entry :=
 (description : string := "")
 (inherit_description_from : option _root_.name := none)
 
-/-- format a `tactic_doc_entry` -/
-meta def tactic_doc_entry.to_string : tactic_doc_entry → string
-| ⟨name, category, decl_names, tags, description, _⟩ :=
-let decl_names := decl_names.map (repr ∘ to_string),
-    tags := tags.map repr in
-"{" ++ to_string (format!"\"name\": {repr name}, \"category\": \"{category}\", \"decl_names\":{decl_names}, \"tags\": {tags}, \"description\": {repr description}") ++ "}"
+/-- Turns a `tactic_doc_entry` into a JSON representation. -/
+meta def tactic_doc_entry.to_json (d : tactic_doc_entry) : json :=
+json.object [
+  ("name", d.name),
+  ("category", d.category.to_string),
+  ("decl_names", d.decl_names.map (json.of_string ∘ to_string)),
+  ("tags", d.tags.map json.of_string),
+  ("description", d.description)
+]
 
 meta instance : has_to_string tactic_doc_entry :=
-⟨tactic_doc_entry.to_string⟩
+⟨json.unparse ∘ tactic_doc_entry.to_json⟩
 
 /-- `update_description_from tde inh_id` replaces the `description` field of `tde` with the
     doc string of the declaration named `inh_id`. -/
@@ -187,11 +190,11 @@ if `tde.description` is the empty string, `add_tactic_doc` uses the doc
 string of `decl` as the description. -/
 meta def tactic.add_tactic_doc (tde : tactic_doc_entry) : tactic unit :=
 do when (tde.description = "" ∧ tde.inherit_description_from.is_none ∧ tde.decl_names.length ≠ 1) $
-     fail
-     ("A tactic doc entry must either:\n" ++
-     " 1. have a description written as a doc-string for the `add_tactic_doc` invocation, or\n" ++
-     " 2. have a single declaration in the `decl_names` field, to inherit a description from, or\n" ++
-     " 3. explicitly indicate the declaration to inherit the description from using `inherit_description_from`."),
+     fail "A tactic doc entry must either:
+ 1. have a description written as a doc-string for the `add_tactic_doc` invocation, or
+ 2. have a single declaration in the `decl_names` field, to inherit a description from, or
+ 3. explicitly indicate the declaration to inherit the description from using
+    `inherit_description_from`.",
    tde ← if tde.description = "" then tde.update_description else return tde,
    let decl_name := (tde.name ++ tde.category.to_string).mk_hashed_name `tactic_doc,
    add_decl $ mk_definition decl_name [] `(tactic_doc_entry) (reflect tde),