--- a/src/Pure/PIDE/markup.ML Fri Aug 12 17:53:55 2016 +0200
+++ b/src/Pure/PIDE/markup.ML Fri Aug 12 20:58:05 2016 +0200
@@ -189,6 +189,7 @@
val padding_line: Properties.entry
val padding_command: Properties.entry
val dialogN: string val dialog: serial -> string -> T
+ val jedit_actionN: string
val functionN: string
val assign_update: Properties.T
val removed_versions: Properties.T
@@ -636,6 +637,8 @@
val dialogN = "dialog";
fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
+val jedit_actionN = "jedit_action";
+
(* protocol message functions *)
--- a/src/Pure/PIDE/markup.scala Fri Aug 12 17:53:55 2016 +0200
+++ b/src/Pure/PIDE/markup.scala Fri Aug 12 20:58:05 2016 +0200
@@ -472,6 +472,8 @@
val DIALOG = "dialog"
val Result = new Properties.String(RESULT)
+ val JEDIT_ACTION = "jedit_action"
+
/* protocol message functions */
--- a/src/Pure/Tools/jedit.ML Fri Aug 12 17:53:55 2016 +0200
+++ b/src/Pure/Tools/jedit.ML Fri Aug 12 20:58:05 2016 +0200
@@ -53,7 +53,13 @@
in
fun check_action (name, pos) =
- if member (op =) (Lazy.force all_actions) name then name
+ if member (op =) (Lazy.force all_actions) name then
+ let
+ val ((bg1, bg2), en) =
+ YXML.output_markup_elem
+ (Active.make_markup Markup.jedit_actionN {implicit = false, properties = []});
+ val msg = "Invoke " ^ bg1 ^ name ^ bg2 ^ name ^ en ^ " jEdit action";
+ in writeln (msg ^ Position.here pos); name end
else
let
val completion =
@@ -66,6 +72,13 @@
val report = Markup.markup_report (Completion.reported_text completion);
in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end
+val _ =
+ Theory.setup
+ (Thy_Output.antiquotation @{binding action} (Scan.lift (Parse.position Parse.embedded))
+ (fn {context = ctxt, ...} => fn (name, pos) =>
+ (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
+ Thy_Output.verbatim_text ctxt name)));
+
end;
end;
--- a/src/Tools/jEdit/src/active.scala Fri Aug 12 17:53:55 2016 +0200
+++ b/src/Tools/jEdit/src/active.scala Fri Aug 12 20:58:05 2016 +0200
@@ -43,6 +43,11 @@
GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
}
+ 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 {
--- a/src/Tools/jEdit/src/rendering.scala Fri Aug 12 17:53:55 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Fri Aug 12 20:58:05 2016 +0200
@@ -169,7 +169,7 @@
private val active_elements =
Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
- Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
+ Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
private val tooltip_message_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,