From 5f67c359bc226aa4826564ad4d78f8cce3e04762 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 27 Oct 2020 10:38:19 +0100
Subject: [PATCH] chore: simplify formatter token separation logic

---
 src/Lean/PrettyPrinter/Formatter.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index c839a9c779..068a739457 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -236,16 +236,16 @@ def pushTokenCore (tk : String) : FormatterM Unit := do
 
 def pushToken (tk : String) : FormatterM Unit := do
   let st ← get
-  -- If there is no space between `tk` and the next word, compare parsing `tk` with and without the next word
+  -- If there is no space between `tk` and the next word, see if we would parse more than `tk` as a single token
   if st.leadWord != "" && tk.trimRight == tk then
-    let t1 ← parseToken tk.trimLeft
-    let t2 ← parseToken $ tk.trimLeft ++ st.leadWord
-    if t1.pos == t2.pos then
-      -- same result => use `tk` as is, extend `leadWord` if not prefixed by whitespace
+    let tk' := tk.trimLeft
+    let t ← parseToken $ tk' ++ st.leadWord
+    if t.pos <= tk'.bsize then
+      -- stopped within `tk` => use it as is, extend `leadWord` if not prefixed by whitespace
       pushTokenCore tk
       modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
     else
-      -- different result => add space
+      -- stopped after `tk` => add space
       pushTokenCore $ tk ++ " "
       modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
   else