# HG changeset patch
# User wenzelm
# Date 1471028285 -7200
# Node ID d2448471ffba55d1316be1aa599b36b8fbb98038
# Parent  6e1e8b5abbfa14828c59275f32e617e6a26416ba
active jEdit actions;

diff -r 6e1e8b5abbfa -r d2448471ffba src/Pure/PIDE/markup.ML
--- 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 *)
 
diff -r 6e1e8b5abbfa -r d2448471ffba src/Pure/PIDE/markup.scala
--- 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 */
 
diff -r 6e1e8b5abbfa -r d2448471ffba src/Pure/Tools/jedit.ML
--- 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;
diff -r 6e1e8b5abbfa -r d2448471ffba src/Tools/jEdit/src/active.scala
--- 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 {
diff -r 6e1e8b5abbfa -r d2448471ffba src/Tools/jEdit/src/rendering.scala
--- 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,