equal
deleted
inserted
replaced
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) |