--- 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 */
--- 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)
+ }
}
--- 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