src/Tools/VSCode/src/document_model.scala
changeset 64671 93e375bd3283
parent 64667 cdb0d559a24b
child 64672 d8e0619abb60
equal deleted inserted replaced
64670:f77b946d18aa 64671:93e375bd3283
    19   /* header */
    19   /* header */
    20 
    20 
    21   def is_theory: Boolean = node_name.is_theory
    21   def is_theory: Boolean = node_name.is_theory
    22 
    22 
    23   lazy val node_header: Document.Node.Header =
    23   lazy val node_header: Document.Node.Header =
    24     if (is_theory) {
    24     if (is_theory)
    25       val toks = Token.explode(Thy_Header.bootstrap_syntax.keywords, doc.text)
    25       session.resources.check_thy_reader(
    26       val toks1 = toks.dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
    26         "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
    27       toks1.iterator.zipWithIndex.collectFirst({ case (tok, i) if tok.is_begin => i }) match {
       
    28         case Some(i) =>
       
    29           session.resources.check_thy_reader("", node_name,
       
    30             new CharSequenceReader(toks1.take(i + 1).map(_.source).mkString), Token.Pos.command)
       
    31         case None => Document.Node.no_header
       
    32       }
       
    33     }
       
    34     else Document.Node.no_header
    27     else Document.Node.no_header
    35 
    28 
    36 
    29 
    37   /* edits */
    30   /* edits */
    38 
    31