--- 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 _ =>
}
}
--- 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