# 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