equal
deleted
inserted
replaced
301 { |
301 { |
302 Document_Model.get(view.getBuffer) match { |
302 Document_Model.get(view.getBuffer) match { |
303 case Some(model) => |
303 case Some(model) => |
304 val name = model.node_name |
304 val name = model.node_name |
305 val url = |
305 val url = |
306 PIDE.plugin.http_server.url + "/" + Preview.service + "?" + |
306 PIDE.plugin.http_server.url + "/" + Preview_Service.service + "?" + |
307 (if (plain_text) plain_text_prefix else "") + Url.encode(name.node) |
307 (if (plain_text) plain_text_prefix else "") + Url.encode(name.node) |
308 PIDE.editor.hyperlink_url(url).follow(view) |
308 PIDE.editor.hyperlink_url(url).follow(view) |
309 case _ => |
309 case _ => |
310 } |
310 } |
311 } |
311 } |
312 |
312 |
313 object Preview extends HTTP.Service("preview") |
313 object Preview_Service extends HTTP.Service("preview") |
314 { |
314 { |
315 def apply(request: HTTP.Request): Option[HTTP.Response] = |
315 def apply(request: HTTP.Request): Option[HTTP.Response] = |
316 for { |
316 for { |
317 query <- request.decode_query |
317 query <- request.decode_query |
318 name = Library.perhaps_unprefix(plain_text_prefix, query) |
318 name = Library.perhaps_unprefix(plain_text_prefix, query) |