# HG changeset patch
# User wenzelm
# Date 1426606689 -3600
# Node ID c443ca40ef8dfbe5211f08171ad700f65c47c185
# Parent  5c1a0069b9d3b613629d5f67e109760fae1010c9
tuned;

diff -r 5c1a0069b9d3 -r c443ca40ef8d src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 16:17:49 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 16:38:09 2015 +0100
@@ -79,17 +79,19 @@
 
     if (is_theory) {
       JEdit_Lib.buffer_lock(buffer) {
-        val toks1 =
-          Token_Markup.line_token_iterator(
-            Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).map(_.info).
-            takeWhile(tok => !tok.is_begin).toList
-        val toks =
-          toks1.dropWhile(tok => !(tok.is_command && tok.source == Thy_Header.THEORY)) :::
-            List(Token(Token.Kind.KEYWORD, "begin"))
-        if (toks.nonEmpty)
-          PIDE.resources.check_thy_reader("", node_name,
-            new CharSequenceReader(Token.implode(toks)), Token.Pos.command)
-        else Document.Node.no_header
+        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
+            })
+          match {
+            case Some(offset) =>
+              val length = buffer.getLength - offset
+              PIDE.resources.check_thy_reader("", node_name,
+                new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
+            case None => Document.Node.no_header
+          }
       }
     }
     else Document.Node.no_header