src/Tools/jEdit/src/document_model.scala
changeset 72652 07edf1952ab1
parent 71733 6c470c918aad
child 72772 a9ef39041114
equal deleted inserted replaced
72651:52cb065aa916 72652:07edf1952ab1
   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 preview =
   322           val preview =
   323             Present.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
   323             Presentation.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
   324               plain_text = query.startsWith(plain_text_prefix))
   324               plain_text = query.startsWith(plain_text_prefix))
   325           HTTP.Response.html(preview.content)
   325           HTTP.Response.html(preview.content)
   326         })
   326         })
   327 
   327 
   328     List(HTTP.fonts(fonts_root), preview)
   328     List(HTTP.fonts(fonts_root), preview)