avoid hard-wired stuff: configure via plugin services;
authorwenzelm
Thu Apr 09 21:58:34 2020 +0200 (7 weeks ago)
changeset 71742de37910974da
parent 71741 1dd97156db80
child 71744 63eb6b3ebcfc
avoid hard-wired stuff: configure via plugin services;
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/services.xml
     1.1 --- a/src/Tools/jEdit/src/active.scala	Thu Apr 09 21:50:00 2020 +0200
     1.2 +++ b/src/Tools/jEdit/src/active.scala	Thu Apr 09 21:58:34 2020 +0200
     1.3 @@ -8,13 +8,22 @@
     1.4  
     1.5  
     1.6  import isabelle._
     1.7 -
     1.8 -import org.gjt.sp.jedit.View
     1.9 -import org.gjt.sp.jedit.browser.VFSBrowser
    1.10 +import org.gjt.sp.jedit.{ServiceManager, View}
    1.11  
    1.12  
    1.13  object Active
    1.14  {
    1.15 +  abstract class Handler
    1.16 +  {
    1.17 +    def handle(
    1.18 +      view: View, text: String, elem: XML.Elem,
    1.19 +      doc_view: Document_View, snapshot: Document.Snapshot): Boolean
    1.20 +  }
    1.21 +
    1.22 +  def handlers: List[Handler] =
    1.23 +    ServiceManager.getServiceNames(classOf[Handler]).toList
    1.24 +      .map(ServiceManager.getService(classOf[Handler], _))
    1.25 +
    1.26    def action(view: View, text: String, elem: XML.Elem)
    1.27    {
    1.28      GUI_Thread.require {}
    1.29 @@ -22,72 +31,80 @@
    1.30      Document_View.get(view.getTextArea) match {
    1.31        case Some(doc_view) =>
    1.32          doc_view.rich_text_area.robust_body() {
    1.33 -          val text_area = doc_view.text_area
    1.34 -          val model = doc_view.model
    1.35 -          val buffer = model.buffer
    1.36 -          val snapshot = model.snapshot()
    1.37 -
    1.38 +          val snapshot = doc_view.model.snapshot()
    1.39            if (!snapshot.is_outdated) {
    1.40 -            // FIXME avoid hard-wired stuff
    1.41 -            elem match {
    1.42 -              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
    1.43 -                Isabelle_Thread.fork(name = "browser") {
    1.44 -                  val graph_file = Isabelle_System.tmp_file("graph")
    1.45 -                  File.write(graph_file, XML.content(body))
    1.46 -                  Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
    1.47 -                }
    1.48 -
    1.49 -              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
    1.50 -                Isabelle_Thread.fork(name = "graphview") {
    1.51 -                  val graph =
    1.52 -                    Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
    1.53 -                  GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
    1.54 -                }
    1.55 -
    1.56 -              case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
    1.57 -                GUI_Thread.later {
    1.58 -                  val name = Markup.Name.unapply(props) getOrElse ""
    1.59 -                  PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view)
    1.60 -                }
    1.61 -
    1.62 -              case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
    1.63 -                GUI_Thread.later {
    1.64 -                  view.getInputHandler.invokeAction(XML.content(body))
    1.65 -                }
    1.66 -
    1.67 -              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
    1.68 -                val link =
    1.69 -                  props match {
    1.70 -                    case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
    1.71 -                    case _ => None
    1.72 -                  }
    1.73 -                GUI_Thread.later {
    1.74 -                  link.foreach(_.follow(view))
    1.75 -                  view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
    1.76 -                }
    1.77 -
    1.78 -              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
    1.79 -                if (buffer.isEditable) {
    1.80 -                  props match {
    1.81 -                    case Position.Id(id) =>
    1.82 -                      Isabelle.edit_command(snapshot, text_area,
    1.83 -                        props.contains(Markup.PADDING_COMMAND), id, text)
    1.84 -                    case _ =>
    1.85 -                      if (props.contains(Markup.PADDING_LINE))
    1.86 -                        Isabelle.insert_line_padding(text_area, text)
    1.87 -                      else text_area.setSelectedText(text)
    1.88 -                  }
    1.89 -                  text_area.requestFocus
    1.90 -                }
    1.91 -
    1.92 -              case Protocol.Dialog(id, serial, result) =>
    1.93 -                model.session.dialog_result(id, serial, result)
    1.94 -
    1.95 -              case _ =>
    1.96 -            }
    1.97 +            handlers.find(_.handle(view, text, elem, doc_view, snapshot))
    1.98            }
    1.99          }
   1.100        case None =>
   1.101      }
   1.102    }
   1.103 +
   1.104 +  class Misc_Handler extends Active.Handler
   1.105 +  {
   1.106 +    override def handle(
   1.107 +      view: View, text: String, elem: XML.Elem,
   1.108 +      doc_view: Document_View, snapshot: Document.Snapshot): Boolean =
   1.109 +    {
   1.110 +      val text_area = doc_view.text_area
   1.111 +      val model = doc_view.model
   1.112 +      val buffer = model.buffer
   1.113 +
   1.114 +      elem match {
   1.115 +        case XML.Elem(Markup(Markup.BROWSER, _), body) =>
   1.116 +          Isabelle_Thread.fork(name = "browser") {
   1.117 +            val graph_file = Isabelle_System.tmp_file("graph")
   1.118 +            File.write(graph_file, XML.content(body))
   1.119 +            Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
   1.120 +          }
   1.121 +          true
   1.122 +
   1.123 +        case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
   1.124 +          GUI_Thread.later {
   1.125 +            val name = Markup.Name.unapply(props) getOrElse ""
   1.126 +            PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view)
   1.127 +          }
   1.128 +          true
   1.129 +
   1.130 +        case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
   1.131 +          GUI_Thread.later {
   1.132 +            view.getInputHandler.invokeAction(XML.content(body))
   1.133 +          }
   1.134 +          true
   1.135 +
   1.136 +        case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
   1.137 +          val link =
   1.138 +            props match {
   1.139 +              case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
   1.140 +              case _ => None
   1.141 +            }
   1.142 +          GUI_Thread.later {
   1.143 +            link.foreach(_.follow(view))
   1.144 +            view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
   1.145 +          }
   1.146 +          true
   1.147 +
   1.148 +        case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
   1.149 +          if (buffer.isEditable) {
   1.150 +            props match {
   1.151 +              case Position.Id(id) =>
   1.152 +                Isabelle.edit_command(snapshot, text_area,
   1.153 +                  props.contains(Markup.PADDING_COMMAND), id, text)
   1.154 +              case _ =>
   1.155 +                if (props.contains(Markup.PADDING_LINE))
   1.156 +                  Isabelle.insert_line_padding(text_area, text)
   1.157 +                else text_area.setSelectedText(text)
   1.158 +            }
   1.159 +            text_area.requestFocus
   1.160 +          }
   1.161 +          true
   1.162 +
   1.163 +        case Protocol.Dialog(id, serial, result) =>
   1.164 +          model.session.dialog_result(id, serial, result)
   1.165 +          true
   1.166 +
   1.167 +        case _ => false
   1.168 +      }
   1.169 +    }
   1.170 +  }
   1.171  }
     2.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Apr 09 21:50:00 2020 +0200
     2.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Thu Apr 09 21:58:34 2020 +0200
     2.3 @@ -39,14 +39,31 @@
     2.4    private def reset_implicit(): Unit =
     2.5      set_implicit(Document.Snapshot.init, no_graph)
     2.6  
     2.7 -  def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
     2.8 +  class Handler extends Active.Handler
     2.9    {
    2.10 -    set_implicit(snapshot, graph)
    2.11 -    view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
    2.12 +    override def handle(
    2.13 +      view: View, text: String, elem: XML.Elem,
    2.14 +      doc_view: Document_View, snapshot: Document.Snapshot): Boolean =
    2.15 +    {
    2.16 +      elem match {
    2.17 +        case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
    2.18 +          Isabelle_Thread.fork(name = "graphview") {
    2.19 +            val graph =
    2.20 +              Exn.capture {
    2.21 +                Graph_Display.decode_graph(body).transitive_reduction_acyclic
    2.22 +              }
    2.23 +            GUI_Thread.later {
    2.24 +              set_implicit(snapshot, graph)
    2.25 +              view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
    2.26 +            }
    2.27 +          }
    2.28 +          true
    2.29 +        case _ => false
    2.30 +      }
    2.31 +    }
    2.32    }
    2.33  }
    2.34  
    2.35 -
    2.36  class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
    2.37  {
    2.38    private val snapshot = Graphview_Dockable.implicit_snapshot
     3.1 --- a/src/Tools/jEdit/src/services.xml	Thu Apr 09 21:50:00 2020 +0200
     3.2 +++ b/src/Tools/jEdit/src/services.xml	Thu Apr 09 21:58:34 2020 +0200
     3.3 @@ -44,4 +44,10 @@
     3.4    <SERVICE CLASS="console.Shell" NAME="Scala">
     3.5      new isabelle.jedit.Scala_Console();
     3.6    </SERVICE>
     3.7 +  <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="misc">
     3.8 +    new isabelle.jedit.Active$Misc_Handler();
     3.9 +  </SERVICE>
    3.10 +  <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="graphview">
    3.11 +    new isabelle.jedit.Graphview_Dockable$Handler()
    3.12 +  </SERVICE>
    3.13  </SERVICES>