diff --git a/Mathport/Syntax/Translate/Basic.lean b/Mathport/Syntax/Translate/Basic.lean
index 7f02d51e6..b2640c7aa 100644
--- a/Mathport/Syntax/Translate/Basic.lean
+++ b/Mathport/Syntax/Translate/Basic.lean
@@ -473,6 +473,12 @@ def push (stx : Syntax) : M Unit := do
         pure f!"-- failed to format: {← e.toMessageData.toString}\n{reprint stx}")
   printOutput f!"{fmt}\n\n"
 
+def stripLastNewline : Format → Format
+  | .append f₁ f₂ => .append f₁ (stripLastNewline f₂)
+  | .text s => .text <|
+      let p := s.prev s.endPos; if s.get p == '\n' then s.extract p s.endPos else s
+  | f => f
+
 def pushM (stx : M Syntax) : M Unit := stx >>= push
 
 def withReplacement (name : Option Name) (x : M Unit) : M Unit :=
@@ -481,7 +487,10 @@ def withReplacement (name : Option Name) (x : M Unit) : M Unit :=
   | some n => do
     match (← read).config.replacementStyle with
     | .skip => pure ()
-    | .comment => printOutput f!"#print {n} /-\n"; x; printOutput f!"-/\n"
+    | .comment =>
+      printOutput f!"#print {n} /-\n"
+      x
+      modify fun s => { s with output := stripLastNewline s.output ++ "-/\n\n" }
     | .keep => x
 
 def getNotationEntry? (n : Name) : M (Option NotationEntry) := do
diff --git a/Mathport/Syntax/Translate/Tactic/Lean3.lean b/Mathport/Syntax/Translate/Tactic/Lean3.lean
index f6ef8dd1c..577f8ee00 100644
--- a/Mathport/Syntax/Translate/Tactic/Lean3.lean
+++ b/Mathport/Syntax/Translate/Tactic/Lean3.lean
@@ -114,10 +114,9 @@ def trLoc : (loc : Location) → M (Option (TSyntax ``Parser.Tactic.location))
 @[tr_tactic revert] def trRevert : TacM Syntax := do
   `(tactic| revert $[$((← parse ident*).map mkIdent)]*)
 
-def trRwRule (r : RwRule) : M (TSyntax ``Parser.Tactic.rwRule) :=
-  return mkNode ``Parser.Tactic.rwRule #[
-    mkOptionalNode $ if r.symm then some (mkAtom "←") else none,
-    ← trExpr r.rule]
+def trRwRule (r : RwRule) : M (TSyntax ``Parser.Tactic.rwRule) := do
+  let e ← trExpr r.rule
+  if r.symm then `(Parser.Tactic.rwRule| ← $e) else `(Parser.Tactic.rwRule| $e:term)
 
 def trRwArgs : TacM (Array (TSyntax ``Parser.Tactic.rwRule) × Option (TSyntax ``Parser.Tactic.location)) := do
   let q ← liftM $ (← parse rwRules).mapM trRwRule