feat: show proof state/unclosed goal message on empty tactic sequences

closes #361

src/Lean/Elab/Tactic/Basic.lean

@@ -175,7 +175,7 @@ mutual
     expandTacticMacroFns stx (macroAttribute.getEntries (← getEnv) stx.getKind)
 
   partial def evalTacticAux (stx : Syntax) : TacticM Unit :=
-    withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
+    withRef stx <| withIncRecDepth <| withFreshMacroScope $ match stx with
       | Syntax.node _ k args =>
         if k == nullKind then
           -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
@@ -186,6 +186,7 @@ mutual
           match tacticElabAttribute.getEntries (← getEnv) stx.getKind with
           | []      => expandTacticMacro stx
           | evalFns => evalTacticUsing s stx evalFns
+      | Syntax.missing => pure ()
       | _ => throwError m!"unexpected tactic{indentD stx}"
 
   partial def evalTactic (stx : Syntax) : TacticM Unit :=

tests/361.lean

@@ -0,0 +1,5 @@
+theorem ex1 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q := by
+
+theorem ex2 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q := by
+  cases h1
+  case inl =>

tests/lean/361.lean.expected.out

@@ -0,0 +1 @@
+file '361.lean' not found