src/Tools/jEdit/src/document_model.scala
changeset 72959 a093b8fc9e21
parent 72957 75fc90edc0a8
child 72960 f7fc8e7c50b0
equal deleted inserted replaced
72958:0d8bc0252e2e 72959:a093b8fc9e21
   317           name = Library.perhaps_unprefix(plain_text_prefix, query)
   317           name = Library.perhaps_unprefix(plain_text_prefix, query)
   318           model <- get(PIDE.resources.node_name(name))
   318           model <- get(PIDE.resources.node_name(name))
   319         }
   319         }
   320         yield {
   320         yield {
   321           val snapshot = model.await_stable_snapshot()
   321           val snapshot = model.await_stable_snapshot()
       
   322           val context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
   322           val document =
   323           val document =
   323             Presentation.html_document(PIDE.resources, snapshot,
   324             Presentation.html_document(PIDE.resources, snapshot, context,
   324               fonts_url = HTML.fonts_dir(fonts_root),
       
   325               plain_text = query.startsWith(plain_text_prefix))
   325               plain_text = query.startsWith(plain_text_prefix))
   326           HTTP.Response.html(document.content)
   326           HTTP.Response.html(document.content)
   327         })
   327         })
   328 
   328 
   329     List(HTTP.fonts(fonts_root), html)
   329     List(HTTP.fonts(fonts_root), html)