# HG changeset patch
# User wenzelm
# Date 1468325622 -7200
# Node ID 8d68204d97d7d97fa8541b9060cb8b6785544d1e
# Parent  723f9c673c1c7ea644ff14ce3a13a51e10c6bfed
clarified;

diff -r 723f9c673c1c -r 8d68204d97d7 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 13:26:39 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:13:42 2016 +0200
@@ -160,7 +160,8 @@
       }
 
     val depth1 =
-      if (tokens.exists(keywords.is_command(_, Keyword.theory))) 0
+      if (tokens.exists(tok =>
+            keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory))) 0
       else if (command_depth.isDefined) command_depth.get
       else if (command1) structure.after_span_depth
       else structure.span_depth