--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 22 16:14:01 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Dec 22 16:20:37 2017 +0100
@@ -293,7 +293,7 @@
val name = model.node_name
val url =
PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" +
- Url.encode(if (name.is_theory) name.theory else name.node)
+ Url.encode(name.node)
PIDE.editor.hyperlink_url(url).follow(view)
case _ =>
}
@@ -307,11 +307,9 @@
val preview =
HTTP.get(preview_root, arg =>
for {
- url_name <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
+ node <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
model <-
- get_models().iterator.collectFirst(
- { case (name, model)
- if url_name == (if (name.is_theory) name.theory else name.node) => model })
+ get_models().iterator.collectFirst({ case (name, model) if name.node == node => model })
}
yield {
val snapshot = model.await_stable_snapshot()