# HG changeset patch
# User wenzelm
# Date 1426605469 -3600
# Node ID 5c1a0069b9d3b613629d5f67e109760fae1010c9
# Parent  24bee1b11fcec43c271cb84937cfe7c74acbc68a
tight span for theory header, which is relevant for error positions (including semantic completion);

diff -r 24bee1b11fce -r 5c1a0069b9d3 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Mar 17 15:21:41 2015 +0100
+++ b/src/Pure/Thy/thy_header.scala	Tue Mar 17 16:17:49 2015 +0100
@@ -60,7 +60,7 @@
   private val bootstrap_keywords =
     Keyword.Keywords.empty.add_keywords(bootstrap_header)
 
-  def bootstrap_syntax(): Outer_Syntax =
+  lazy val bootstrap_syntax: Outer_Syntax =
     Outer_Syntax.init().add_keywords(bootstrap_header)
 
 
diff -r 24bee1b11fce -r 5c1a0069b9d3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 17 15:21:41 2015 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 17 16:17:49 2015 +0100
@@ -438,7 +438,7 @@
               info.parent.map(deps(_)) match {
                 case None =>
                   (Set.empty[String], Map.empty[String, Document.Node.Name],
-                    Thy_Header.bootstrap_syntax())
+                    Thy_Header.bootstrap_syntax)
                 case Some(parent) =>
                   (parent.loaded_theories, parent.known_theories, parent.syntax)
               }
diff -r 24bee1b11fce -r 5c1a0069b9d3 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 15:21:41 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 16:17:49 2015 +0100
@@ -12,6 +12,7 @@
 import isabelle._
 
 import scala.collection.mutable
+import scala.util.parsing.input.CharSequenceReader
 
 import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.jedit.Buffer
@@ -78,13 +79,17 @@
 
     if (is_theory) {
       JEdit_Lib.buffer_lock(buffer) {
-        Exn.capture {
+        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,
-            JEdit_Lib.buffer_reader(buffer), Token.Pos.command)
-        } match {
-          case Exn.Res(header) => header
-          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
-        }
+            new CharSequenceReader(Token.implode(toks)), Token.Pos.command)
+        else Document.Node.no_header
       }
     }
     else Document.Node.no_header