# HG changeset patch
# User wenzelm
# Date 1468322799 -7200
# Node ID 723f9c673c1c7ea644ff14ce3a13a51e10c6bfed
# Parent  be6ceddff1020943475f5248c55565893e36f471
closing 'qed' or '}' is outside of fold;

diff -r be6ceddff102 -r 723f9c673c1c src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 12:58:53 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 13:26:39 2016 +0200
@@ -148,8 +148,20 @@
     val improper1 = tokens.forall(_.is_improper)
     val command1 = tokens.exists(_.is_command)
 
+    val command_depth =
+      tokens.iterator.filter(_.is_proper).toStream.headOption match {
+        case Some(tok) =>
+          if (keywords.is_command(tok, Keyword.QED_BLOCK == _))
+            Some(structure.after_span_depth - 2)
+          else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _))
+            Some(structure.after_span_depth - 1)
+          else None
+        case None => None
+      }
+
     val depth1 =
       if (tokens.exists(keywords.is_command(_, Keyword.theory))) 0
+      else if (command_depth.isDefined) command_depth.get
       else if (command1) structure.after_span_depth
       else structure.span_depth
 
@@ -161,7 +173,8 @@
             else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
             else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
             else if (keywords.is_command(tok, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
-            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
+            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y - 1, y - 2)
+            else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _)) (y, y - 1)
             else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
             else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
             else (x, y)