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