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