chore: update test capture

Author: insightmind

test/playground/infoTree.lean.leanInk.expected

@@ -18,7 +18,24 @@
  {"contents":
   "\n\ndef f2 : (x y : Nat) → (b : Bool) → Nat :=\n  fun x y b =>\n    let (z, w) := (x + y, x - y)\n    let z1 := z + w\n    z + z1\n\ndef f3 (s : Nat × Array (Array Nat)) : Array Nat :=\n  s.2[1].push s.1\n\ndef f4 (arg : B) : Nat :=\n  arg.pair.fst.val 0\n\ndef f5 (x : Nat) : B := {\n  pair := ({ val := id }, { val := id })\n}\n\nopen Nat in\n",
   "_type": "text"},
- {"contents": "#print", "_type": "text"},
+ {"messages":
+  [{"contents": "def Nat.xor : Nat → Nat → Nat :=\nbitwise bne\n",
+    "_type": "message"}],
+  "goals": [],
+  "contents": "#print",
+  "_type": "sentence"},
  {"contents": " xor\ninstance : Inhabited Nat where\n\n", "_type": "text"},
- {"contents": "macro", "_type": "text"},
- {"contents": "", "_type": "text"}]
+ {"messages":
+  [{"contents": "infoTree.lean:39:0: error: expected identifier or term\n",
+    "_type": "message"}],
+  "goals": [],
+  "contents": "macro",
+  "_type": "sentence"},
+ {"messages":
+  [{"contents": "infoTree.lean:39:0: error: expected identifier or term\n",
+    "_type": "message"},
+   {"contents": "infoTree.lean:39:5: error: unexpected end of input\n",
+    "_type": "message"}],
+  "goals": [],
+  "contents": "",
+  "_type": "sentence"}]

test/playground/playground_1.lean.leanInk.expected

@@ -1,9 +1,15 @@
 [{"contents":
   "/-|\n=======\n Title\n=======\n\nProse. *Emphasis*; **strong emphasis**; ``code``; `coq code`; `link <url>`__.\n|-/\n\n",
   "_type": "text"},
- {"contents": "#check", "_type": "text"},
+ {"messages": [{"contents": "Bool : Type\n", "_type": "message"}],
+  "goals": [],
+  "contents": "#check",
+  "_type": "sentence"},
  {"contents": " Bool\n\n", "_type": "text"},
- {"contents": "#print", "_type": "text"},
+ {"messages": [{"contents": "Hello World\n", "_type": "message"}],
+  "goals": [],
+  "contents": "#print",
+  "_type": "sentence"},
  {"contents":
   " \"Hello World\"\n\nexample (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := ",
   "_type": "text"},

test/theorem_proving/001.lean.leanInk.expected

@@ -1,4 +1,9 @@
 [{"contents": "theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p :=\n  ",
   "_type": "text"},
- {"contents": "sorry", "_type": "text"},
+ {"messages":
+  [{"contents": "001.lean:2:2: warning: declaration uses 'sorry'\n",
+    "_type": "message"}],
+  "goals": [],
+  "contents": "sorry",
+  "_type": "sentence"},
  {"contents": "", "_type": "text"}]

test/theorem_proving/005.lean.leanInk.expected

@@ -49,5 +49,8 @@
   "contents": "exact And.intro hq hp",
   "_type": "sentence"},
  {"contents": "\n\n", "_type": "text"},
- {"contents": "#check", "_type": "text"},
+ {"messages": [{"contents": "And : Prop → Prop → Prop\n", "_type": "message"}],
+  "goals": [],
+  "contents": "#check",
+  "_type": "sentence"},
  {"contents": " And", "_type": "text"}]