From 08d54b60433eb9210b2ab9500cd86d6475de4c94 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 11:37:43 -0700
Subject: [PATCH] feat: add `checkColGt` at `app`

@Kha Only one example broke :)
---
 src/Lean/Parser/Term.lean | 7 +++++--
 tests/lean/stdio.lean     | 8 ++++----
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 2ea5fb4de5..a43eb56a4a 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -61,7 +61,7 @@ checkPrec prec >> symbol sym >> termParser (prec+1)
 def typeAscription := parser! " : " >> termParser
 def tupleTail      := parser! ", " >> sepBy1 termParser ", "
 def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
-@[builtinTermParser] def paren := parser! "(" >> optional (termParser >> parenSpecial) >> ")"
+@[builtinTermParser] def paren := parser! "(" >> withoutPosition (optional (termParser >> parenSpecial)) >> ")"
 @[builtinTermParser] def anonymousCtor := parser! "⟨" >> sepBy termParser ", " >> "⟩"
 def optIdent : Parser := optional (try (ident >> " : "))
 @[builtinTermParser] def «if»  := parser!:leadPrec "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
@@ -165,7 +165,10 @@ def attributes       := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
 
 def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
 def ellipsis       := parser! ".."
-@[builtinTermParser] def app      := tparser!:(maxPrec-1) many1 (checkWsBefore "expected space" >> (namedArgument <|> termParser maxPrec <|> ellipsis))
+@[builtinTermParser] def app      := tparser!:(maxPrec-1) many1 $
+  checkWsBefore "expected space" >>
+  checkColGt "expected to be indented" >>
+  (namedArgument <|> termParser maxPrec <|> ellipsis)
 
 @[builtinTermParser] def proj     := tparser! symbolNoWs "." >> (fieldIdx <|> ident)
 @[builtinTermParser] def arrow    := tparser! unicodeInfixR " → " " -> " 25
diff --git a/tests/lean/stdio.lean b/tests/lean/stdio.lean
index 5be5c6063e..d03fd548b6 100644
--- a/tests/lean/stdio.lean
+++ b/tests/lean/stdio.lean
@@ -17,10 +17,10 @@ FS.withFile "stdout1.txt" IO.FS.Mode.write $ fun h₁ => do
   withStdout (Stream.ofHandle h₁) $ do
     println "line 1";
     catch
-    ( do
-      withStdout (Stream.ofHandle h₂) $ println "line 2";
-      throw $ IO.userError "my error" )
-    ( fun e => println e );
+      ( do
+        withStdout (Stream.ofHandle h₂) $ println "line 2";
+        throw $ IO.userError "my error" )
+      ( fun e => println e );
     println "line 3" };
 println "line 4";
 println "\n> stdout1.txt";