# HG changeset patch
# User wenzelm
# Date 1496917559 -7200
# Node ID b6396880b64417c95124560f8d63fc4b8ed1be69
# Parent  ded1c636aecec7e60d6c9cc5cabf0069ca11dcb1
clarified;

diff -r ded1c636aece -r b6396880b644 src/Tools/jEdit/src/document_model.scala
--- 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 _ =>
     }
   }
 
diff -r ded1c636aece -r b6396880b644 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Wed Jun 07 23:23:48 2017 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Thu Jun 08 12:25:59 2017 +0200
@@ -226,6 +226,7 @@
 isabelle.newline.label=Newline with indentation of Isabelle keywords
 isabelle.newline.shortcut=ENTER
 isabelle.options.label=Isabelle options
+isabelle.preview.label=HTML preview of PIDE document
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size
 isabelle.reset-node-required.label=Reset node required