src/Tools/VSCode/src/preview_panel.scala
changeset 73036 b028e8d22d8d
parent 72961 f78730341c87
child 73055 3e4df2e689ff
equal deleted inserted replaced
73035:03e78b35ebbc 73036:b028e8d22d8d
    29             case Some(model) =>
    29             case Some(model) =>
    30               val snapshot = model.snapshot()
    30               val snapshot = model.snapshot()
    31               if (snapshot.is_outdated) m
    31               if (snapshot.is_outdated) m
    32               else {
    32               else {
    33                 val html_context = Presentation.html_context()
    33                 val html_context = Presentation.html_context()
    34                 val document = Presentation.html_document(resources, snapshot, html_context)
    34                 val document =
       
    35                   Presentation.html_document(
       
    36                     resources, snapshot, html_context, Presentation.html_elements2)
    35                 channel.write(LSP.Preview_Response(file, column, document.title, document.content))
    37                 channel.write(LSP.Preview_Response(file, column, document.title, document.content))
    36                 m - file
    38                 m - file
    37               }
    39               }
    38             case None => m - file
    40             case None => m - file
    39           }
    41           }