diff --git a/src/Tools/jEdit/src/active.scala b/src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala +++ b/src/Tools/jEdit/src/active.scala @@ -1,93 +1,110 @@ /* Title: Tools/jEdit/src/active.scala Author: Makarius Active areas within the document. */ package isabelle.jedit 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 {} 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 --git a/src/Tools/jEdit/src/graphview_dockable.scala b/src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala +++ b/src/Tools/jEdit/src/graphview_dockable.scala @@ -1,148 +1,165 @@ /* Title: Tools/jEdit/src/graphview_dockable.scala Author: Makarius Stateless dockable window for graphview. */ package isabelle.jedit import isabelle._ import isabelle.jedit_base.Dockable import javax.swing.JComponent import java.awt.{Point, Font} import java.awt.event.{WindowFocusListener, WindowEvent} import org.gjt.sp.jedit.View import scala.swing.TextArea object Graphview_Dockable { /* implicit arguments -- owned by GUI thread */ private var implicit_snapshot = Document.Snapshot.init private val no_graph: Exn.Result[Graph_Display.Graph] = Exn.Exn(ERROR("No graph")) private var implicit_graph = no_graph private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph]) { GUI_Thread.require {} implicit_snapshot = snapshot implicit_graph = graph } 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 private val graph_result = Graphview_Dockable.implicit_graph private val window_focus_listener = new WindowFocusListener { def windowGainedFocus(e: WindowEvent) { Graphview_Dockable.set_implicit(snapshot, graph_result) } def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() } } val graphview = graph_result match { case Exn.Res(graph) => val graphview = new isabelle.graphview.Graphview(graph) { def options: Options = PIDE.options.value override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = { Pretty_Tooltip.invoke(() => { val model = File_Model.empty(PIDE.session) val rendering = JEdit_Rendering(snapshot, model, options) val info = Text.Info(Text.Range.offside, body) Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info) }) null } override def make_font(): Font = if (editor_style) GUI.imitate_font(Font_Info.main().font) else GUI.imitate_font(Font_Info.main().font, family = options.string("graphview_font_family"), scale = options.real("graphview_font_scale")) override def foreground_color = if (editor_style) view.getTextArea.getPainter.getForeground else super.foreground_color override def background_color = if (editor_style) view.getTextArea.getPainter.getBackground else super.background_color override def selection_color = if (editor_style) view.getTextArea.getPainter.getSelectionColor else super.selection_color override def highlight_color = if (editor_style) view.getTextArea.getPainter.getLineHighlightColor else super.highlight_color override def error_color = PIDE.options.color_value("error_color") editor_style = true } new isabelle.graphview.Main_Panel(graphview) case Exn.Exn(exn) => new TextArea(Exn.message(exn)) } set_content(graphview) override def focusOnDefaultComponent() { graphview match { case main_panel: isabelle.graphview.Main_Panel => main_panel.tree_panel.tree.requestFocusInWindow case _ => } } /* main */ private val main = Session.Consumer[Session.Global_Options](getClass.getName) { case _: Session.Global_Options => GUI_Thread.later { graphview match { case main_panel: isabelle.graphview.Main_Panel => main_panel.update_layout() case _ => } } } override def init() { GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener)) PIDE.session.global_options += main } override def exit() { GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener)) PIDE.session.global_options -= main } } diff --git a/src/Tools/jEdit/src/services.xml b/src/Tools/jEdit/src/services.xml --- a/src/Tools/jEdit/src/services.xml +++ b/src/Tools/jEdit/src/services.xml @@ -1,47 +1,53 @@ new isabelle.jedit.Fold_Handling.Fold_Handler(); new isabelle.jedit.Context_Menu(); new isabelle.jedit.Isabelle_Export.VFS(); new isabelle.jedit.Isabelle_Session.VFS(); new isabelle.jedit.Isabelle_Sidekick_Default(); new isabelle.jedit.Isabelle_Sidekick_Context(); new isabelle.jedit.Isabelle_Sidekick_Markup(); new isabelle.jedit.Isabelle_Sidekick_ML(); new isabelle.jedit.Isabelle_Sidekick_SML(); new isabelle.jedit.Isabelle_Sidekick_News(); new isabelle.jedit.Isabelle_Sidekick_Options(); new isabelle.jedit.Isabelle_Sidekick_Root(); new isabelle.jedit.JEdit_Bibtex.Sidekick_Parser(); new isabelle.jedit.Scala_Console(); + + new isabelle.jedit.Active$Misc_Handler(); + + + new isabelle.jedit.Graphview_Dockable$Handler() +