# HG changeset patch
# User wenzelm
# Date 1586462314 -7200
# Node ID de37910974da85baa409206609690391f20d406c
# Parent 1dd97156db803c644a1b4c800989bd3332dbd23b
avoid hard-wired stuff: configure via plugin services;
diff -r 1dd97156db80 -r de37910974da src/Tools/jEdit/src/active.scala
--- 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
+ }
+ }
+ }
}
diff -r 1dd97156db80 -r de37910974da src/Tools/jEdit/src/graphview_dockable.scala
--- 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
diff -r 1dd97156db80 -r de37910974da src/Tools/jEdit/src/services.xml
--- 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 @@
new isabelle.jedit.Scala_Console();
+
+ new isabelle.jedit.Active$Misc_Handler();
+
+
+ new isabelle.jedit.Graphview_Dockable$Handler()
+