src/Tools/jEdit/src/document_model.scala
changeset 66036 b6396880b644
parent 66019 69b5ef78fb07
child 66040 f826ba18fe08
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jun 07 23:23:48 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jun 08 12:25:59 2017 +0200
@@ -272,11 +272,11 @@
   def open_preview(view: View)
   {
     Document_Model.get(view.getBuffer) match {
-      case Some(model) =>
+      case Some(model) if model.is_theory =>
         JEdit_Editor.hyperlink_url(
           PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview/" +
             model.node_name.theory).follow(view)
-      case None =>
+      case _ =>
     }
   }