clarified;
authorwenzelm
Tue, 12 Jul 2016 14:13:42 +0200
changeset 63459 8d68204d97d7
parent 63458 723f9c673c1c
child 63460 f41070510341
clarified;
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