# HG changeset patch
# User wenzelm
# Date 1513956037 -3600
# Node ID 51b30032cf206e2424d2a5e60255900bc4ac1f9e
# Parent  5035b6754fca924c473dfcd39bb50b52c4449bbf
clarified URL: unique node name;

diff -r 5035b6754fca -r 51b30032cf20 src/Tools/jEdit/src/document_model.scala
--- 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()