# HG changeset patch
# User wenzelm
# Date 1482754868 -3600
# Node ID 93e375bd3283cd4a37d5680d715b0ca48768b803
# Parent  f77b946d18aa6c72bef0724b1a3b722fc47d31e5
clarified header text;

diff -r f77b946d18aa -r 93e375bd3283 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Fri Dec 23 20:12:27 2016 +0100
+++ b/src/Pure/Isar/token.scala	Mon Dec 26 13:21:08 2016 +0100
@@ -152,6 +152,8 @@
     (toks.toList, ctxt)
   }
 
+  val newline: Token = explode(Keyword.Keywords.empty, "\n").head
+
 
   /* implode */
 
diff -r f77b946d18aa -r 93e375bd3283 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Dec 23 20:12:27 2016 +0100
+++ b/src/Pure/Thy/thy_header.scala	Mon Dec 26 13:21:08 2016 +0100
@@ -172,6 +172,35 @@
 
   def read(source: CharSequence, start: Token.Pos): Thy_Header =
     read(new CharSequenceReader(source), start)
+
+
+  /* line-oriented text */
+
+  def header_text(doc: Line.Document): String =
+  {
+    val keywords = bootstrap_syntax.keywords
+    val toks = new mutable.ListBuffer[Token]
+    val iterator =
+      (for {
+        (toks, _) <-
+          doc.lines.iterator.scanLeft((List.empty[Token], Scan.Finished: Scan.Line_Context))(
+            {
+              case ((_, ctxt), line) => Token.explode_line(keywords, line.text, ctxt)
+            })
+        tok <- toks.iterator ++ Iterator.single(Token.newline)
+      } yield tok).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
+
+    @tailrec def until_begin
+    {
+      if (iterator.hasNext) {
+        val tok = iterator.next
+        toks += tok
+        if (!tok.is_begin) until_begin
+      }
+    }
+    until_begin
+    Token.implode(toks.toList)
+  }
 }
 
 
diff -r f77b946d18aa -r 93e375bd3283 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 20:12:27 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Dec 26 13:21:08 2016 +0100
@@ -21,16 +21,9 @@
   def is_theory: Boolean = node_name.is_theory
 
   lazy val node_header: Document.Node.Header =
-    if (is_theory) {
-      val toks = Token.explode(Thy_Header.bootstrap_syntax.keywords, doc.text)
-      val toks1 = toks.dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
-      toks1.iterator.zipWithIndex.collectFirst({ case (tok, i) if tok.is_begin => i }) match {
-        case Some(i) =>
-          session.resources.check_thy_reader("", node_name,
-            new CharSequenceReader(toks1.take(i + 1).map(_.source).mkString), Token.Pos.command)
-        case None => Document.Node.no_header
-      }
-    }
+    if (is_theory)
+      session.resources.check_thy_reader(
+        "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
     else Document.Node.no_header