avoid hard-wired stuff: configure via plugin services;
authorwenzelm
Thu, 09 Apr 2020 21:58:34 +0200
changeset 71958 de37910974da
parent 71957 1dd97156db80
child 71959 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
--- a/src/Tools/jEdit/src/active.scala	Thu Apr 09 21:50:00 2020 +0200
+++ b/src/Tools/jEdit/src/active.scala	Thu Apr 09 21:58:34 2020 +0200
@@ -8,13 +8,22 @@
 
 
 import isabelle._
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.browser.VFSBrowser
+import org.gjt.sp.jedit.{ServiceManager, View}
 
 
 object Active
 {
+  abstract class Handler
+  {
+    def handle(
+      view: View, text: String, elem: XML.Elem,
+      doc_view: Document_View, snapshot: Document.Snapshot): Boolean
+  }
+
+  def handlers: List[Handler] =
+    ServiceManager.getServiceNames(classOf[Handler]).toList
+      .map(ServiceManager.getService(classOf[Handler], _))
+
   def action(view: View, text: String, elem: XML.Elem)
   {
     GUI_Thread.require {}
@@ -22,72 +31,80 @@
     Document_View.get(view.getTextArea) match {
       case Some(doc_view) =>
         doc_view.rich_text_area.robust_body() {
-          val text_area = doc_view.text_area
-          val model = doc_view.model
-          val buffer = model.buffer
-          val snapshot = model.snapshot()
-
+          val snapshot = doc_view.model.snapshot()
           if (!snapshot.is_outdated) {
-            // FIXME avoid hard-wired stuff
-            elem match {
-              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
-                Isabelle_Thread.fork(name = "browser") {
-                  val graph_file = Isabelle_System.tmp_file("graph")
-                  File.write(graph_file, XML.content(body))
-                  Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
-                }
-
-              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
-                Isabelle_Thread.fork(name = "graphview") {
-                  val graph =
-                    Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
-                  GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
-                }
-
-              case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
-                GUI_Thread.later {
-                  val name = Markup.Name.unapply(props) getOrElse ""
-                  PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view)
-                }
-
-              case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
-                GUI_Thread.later {
-                  view.getInputHandler.invokeAction(XML.content(body))
-                }
-
-              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
-                val link =
-                  props match {
-                    case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
-                    case _ => None
-                  }
-                GUI_Thread.later {
-                  link.foreach(_.follow(view))
-                  view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
-                }
-
-              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
-                if (buffer.isEditable) {
-                  props match {
-                    case Position.Id(id) =>
-                      Isabelle.edit_command(snapshot, text_area,
-                        props.contains(Markup.PADDING_COMMAND), id, text)
-                    case _ =>
-                      if (props.contains(Markup.PADDING_LINE))
-                        Isabelle.insert_line_padding(text_area, text)
-                      else text_area.setSelectedText(text)
-                  }
-                  text_area.requestFocus
-                }
-
-              case Protocol.Dialog(id, serial, result) =>
-                model.session.dialog_result(id, serial, result)
-
-              case _ =>
-            }
+            handlers.find(_.handle(view, text, elem, doc_view, snapshot))
           }
         }
       case None =>
     }
   }
+
+  class Misc_Handler extends Active.Handler
+  {
+    override def handle(
+      view: View, text: String, elem: XML.Elem,
+      doc_view: Document_View, snapshot: Document.Snapshot): Boolean =
+    {
+      val text_area = doc_view.text_area
+      val model = doc_view.model
+      val buffer = model.buffer
+
+      elem match {
+        case XML.Elem(Markup(Markup.BROWSER, _), body) =>
+          Isabelle_Thread.fork(name = "browser") {
+            val graph_file = Isabelle_System.tmp_file("graph")
+            File.write(graph_file, XML.content(body))
+            Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
+          }
+          true
+
+        case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
+          GUI_Thread.later {
+            val name = Markup.Name.unapply(props) getOrElse ""
+            PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view)
+          }
+          true
+
+        case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
+          GUI_Thread.later {
+            view.getInputHandler.invokeAction(XML.content(body))
+          }
+          true
+
+        case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
+          val link =
+            props match {
+              case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
+              case _ => None
+            }
+          GUI_Thread.later {
+            link.foreach(_.follow(view))
+            view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
+          }
+          true
+
+        case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
+          if (buffer.isEditable) {
+            props match {
+              case Position.Id(id) =>
+                Isabelle.edit_command(snapshot, text_area,
+                  props.contains(Markup.PADDING_COMMAND), id, text)
+              case _ =>
+                if (props.contains(Markup.PADDING_LINE))
+                  Isabelle.insert_line_padding(text_area, text)
+                else text_area.setSelectedText(text)
+            }
+            text_area.requestFocus
+          }
+          true
+
+        case Protocol.Dialog(id, serial, result) =>
+          model.session.dialog_result(id, serial, result)
+          true
+
+        case _ => false
+      }
+    }
+  }
 }
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Apr 09 21:50:00 2020 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Thu Apr 09 21:58:34 2020 +0200
@@ -39,14 +39,31 @@
   private def reset_implicit(): Unit =
     set_implicit(Document.Snapshot.init, no_graph)
 
-  def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
+  class Handler extends Active.Handler
   {
-    set_implicit(snapshot, graph)
-    view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
+    override def handle(
+      view: View, text: String, elem: XML.Elem,
+      doc_view: Document_View, snapshot: Document.Snapshot): Boolean =
+    {
+      elem match {
+        case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
+          Isabelle_Thread.fork(name = "graphview") {
+            val graph =
+              Exn.capture {
+                Graph_Display.decode_graph(body).transitive_reduction_acyclic
+              }
+            GUI_Thread.later {
+              set_implicit(snapshot, graph)
+              view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
+            }
+          }
+          true
+        case _ => false
+      }
+    }
   }
 }
 
-
 class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
 {
   private val snapshot = Graphview_Dockable.implicit_snapshot
--- a/src/Tools/jEdit/src/services.xml	Thu Apr 09 21:50:00 2020 +0200
+++ b/src/Tools/jEdit/src/services.xml	Thu Apr 09 21:58:34 2020 +0200
@@ -44,4 +44,10 @@
   <SERVICE CLASS="console.Shell" NAME="Scala">
     new isabelle.jedit.Scala_Console();
   </SERVICE>
+  <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="misc">
+    new isabelle.jedit.Active$Misc_Handler();
+  </SERVICE>
+  <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="graphview">
+    new isabelle.jedit.Graphview_Dockable$Handler()
+  </SERVICE>
 </SERVICES>