clarified;
authorwenzelm
Thu Jun 08 12:25:59 2017 +0200 (23 months ago)
changeset 66036b6396880b644
parent 66034 ded1c636aece
child 66037 58d2e41afbfe
clarified;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jEdit.props
     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  
     2.1 --- a/src/Tools/jEdit/src/jEdit.props	Wed Jun 07 23:23:48 2017 +0200
     2.2 +++ b/src/Tools/jEdit/src/jEdit.props	Thu Jun 08 12:25:59 2017 +0200
     2.3 @@ -226,6 +226,7 @@
     2.4  isabelle.newline.label=Newline with indentation of Isabelle keywords
     2.5  isabelle.newline.shortcut=ENTER
     2.6  isabelle.options.label=Isabelle options
     2.7 +isabelle.preview.label=HTML preview of PIDE document
     2.8  isabelle.reset-continuous-checking.label=Reset continuous checking
     2.9  isabelle.reset-font-size.label=Reset font size
    2.10  isabelle.reset-node-required.label=Reset node required