active jEdit actions;
authorwenzelm
Fri Aug 12 20:58:05 2016 +0200 (2016-08-12)
changeset 63681d2448471ffba
parent 63680 6e1e8b5abbfa
child 63682 67cffbbca84d
active jEdit actions;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Tools/jedit.ML
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Fri Aug 12 17:53:55 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Fri Aug 12 20:58:05 2016 +0200
     1.3 @@ -189,6 +189,7 @@
     1.4    val padding_line: Properties.entry
     1.5    val padding_command: Properties.entry
     1.6    val dialogN: string val dialog: serial -> string -> T
     1.7 +  val jedit_actionN: string
     1.8    val functionN: string
     1.9    val assign_update: Properties.T
    1.10    val removed_versions: Properties.T
    1.11 @@ -636,6 +637,8 @@
    1.12  val dialogN = "dialog";
    1.13  fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
    1.14  
    1.15 +val jedit_actionN = "jedit_action";
    1.16 +
    1.17  
    1.18  (* protocol message functions *)
    1.19  
     2.1 --- a/src/Pure/PIDE/markup.scala	Fri Aug 12 17:53:55 2016 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Fri Aug 12 20:58:05 2016 +0200
     2.3 @@ -472,6 +472,8 @@
     2.4    val DIALOG = "dialog"
     2.5    val Result = new Properties.String(RESULT)
     2.6  
     2.7 +  val JEDIT_ACTION = "jedit_action"
     2.8 +
     2.9  
    2.10    /* protocol message functions */
    2.11  
     3.1 --- a/src/Pure/Tools/jedit.ML	Fri Aug 12 17:53:55 2016 +0200
     3.2 +++ b/src/Pure/Tools/jedit.ML	Fri Aug 12 20:58:05 2016 +0200
     3.3 @@ -53,7 +53,13 @@
     3.4  in
     3.5  
     3.6  fun check_action (name, pos) =
     3.7 -  if member (op =) (Lazy.force all_actions) name then name
     3.8 +  if member (op =) (Lazy.force all_actions) name then
     3.9 +    let
    3.10 +      val ((bg1, bg2), en) =
    3.11 +        YXML.output_markup_elem
    3.12 +          (Active.make_markup Markup.jedit_actionN {implicit = false, properties = []});
    3.13 +      val msg = "Invoke " ^ bg1 ^ name ^ bg2 ^ name ^ en ^ " jEdit action";
    3.14 +    in writeln (msg ^ Position.here pos); name end
    3.15    else
    3.16      let
    3.17        val completion =
    3.18 @@ -66,6 +72,13 @@
    3.19        val report = Markup.markup_report (Completion.reported_text completion);
    3.20      in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end
    3.21  
    3.22 +val _ =
    3.23 +  Theory.setup
    3.24 +    (Thy_Output.antiquotation @{binding action} (Scan.lift (Parse.position Parse.embedded))
    3.25 +      (fn {context = ctxt, ...} => fn (name, pos) =>
    3.26 +       (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
    3.27 +        Thy_Output.verbatim_text ctxt name)));
    3.28 +
    3.29  end;
    3.30  
    3.31  end;
     4.1 --- a/src/Tools/jEdit/src/active.scala	Fri Aug 12 17:53:55 2016 +0200
     4.2 +++ b/src/Tools/jEdit/src/active.scala	Fri Aug 12 20:58:05 2016 +0200
     4.3 @@ -43,6 +43,11 @@
     4.4                    GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
     4.5                  }
     4.6  
     4.7 +              case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
     4.8 +                GUI_Thread.later {
     4.9 +                  view.getInputHandler.invokeAction(XML.content(body))
    4.10 +                }
    4.11 +
    4.12                case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
    4.13                  val link =
    4.14                    props match {
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Aug 12 17:53:55 2016 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Aug 12 20:58:05 2016 +0200
     5.3 @@ -169,7 +169,7 @@
     5.4  
     5.5    private val active_elements =
     5.6      Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
     5.7 -      Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
     5.8 +      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
     5.9  
    5.10    private val tooltip_message_elements =
    5.11      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,