src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Mon Jul 11 17:53:02 2016 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 11 18:18:24 2016 +0200
@@ -96,8 +96,7 @@
           Token_Markup.line_token_iterator(
             Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
               {
-                case Text.Info(range, tok)
-                if tok.is_command && tok.source == Thy_Header.THEORY => range.start
+                case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start
               })
             match {
               case Some(offset) =>