src/Tools/VSCode/src/document_model.scala
changeset 64673 b5965890e54d
parent 64672 d8e0619abb60
child 64679 b2bf280b7e13
equal deleted inserted replaced
64672:d8e0619abb60 64673:b5965890e54d
    18 {
    18 {
    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   def node_header(resources: VSCode_Resources): Document.Node.Header =
    24     if (is_theory)
    24     resources.special_header(node_name) getOrElse
    25       session.resources.check_thy_reader(
    25     {
    26         "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
    26       if (is_theory)
    27     else Document.Node.no_header
    27         session.resources.check_thy_reader(
       
    28           "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
       
    29       else Document.Node.no_header
       
    30     }
    28 
    31 
    29 
    32 
    30   /* edits */
    33   /* edits */
    31 
    34 
    32   def text_edits: List[Text.Edit] =
    35   def text_edits: List[Text.Edit] =
    33     if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
    36     if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
    34 
    37 
    35   def node_edits: List[Document.Edit_Text] =
    38   def node_edits(resources: VSCode_Resources): List[Document.Edit_Text] =
    36     if (changed) {
    39     if (changed) {
    37       List(session.header_edit(node_name, node_header),
    40       List(session.header_edit(node_name, node_header(resources)),
    38         node_name -> Document.Node.Clear(),
    41         node_name -> Document.Node.Clear(),
    39         node_name -> Document.Node.Edits(text_edits),
    42         node_name -> Document.Node.Edits(text_edits),
    40         node_name ->
    43         node_name ->
    41           Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty))
    44           Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty))
    42     }
    45     }