tuned;
authorwenzelm
Fri, 22 Dec 2017 16:26:14 +0100
changeset 67259 e13e8816cf2a
parent 67258 51b30032cf20
child 67260 ecd607631bc7
tuned;
src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 16:20:37 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 16:26:14 2017 +0100
@@ -292,8 +292,8 @@
       case Some(model) =>
         val name = model.node_name
         val url =
-          PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" +
-            Url.encode(name.node)
+          PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root +
+            "/preview?" + Url.encode(name.node)
         PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
     }
@@ -307,9 +307,8 @@
     val preview =
       HTTP.get(preview_root, arg =>
         for {
-          node <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
-          model <-
-            get_models().iterator.collectFirst({ case (name, model) if name.node == node => model })
+          query <- Library.try_unprefix(preview_root + "?", arg.uri.toString)
+          model <- get(PIDE.resources.node_name(Url.decode(query)))
         }
         yield {
           val snapshot = model.await_stable_snapshot()