# HG changeset patch
# User wenzelm
# Date 1402946810 -7200
# Node ID 54c6b73774d2aae9223f3e233b255d0885443b37
# Parent  d58b7f7d81dbbe12e1db41d855823fba4d648d2e
formal check of jEdit actions;

diff -r d58b7f7d81db -r 54c6b73774d2 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Jun 16 20:50:56 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon Jun 16 21:26:50 2014 +0200
@@ -1020,7 +1020,7 @@
 
   \emph{Explicit completion} works via the action @{action_ref
   "isabelle.complete"}, which is bound to the key sequence @{verbatim "C+b"}
-  (overriding the jEdit default for @{verbatim "complete-word"}).
+  (overriding the jEdit default for @{action_ref "complete-word"}).
   \emph{Implicit completion} hooks into the regular keyboard input stream of
   the editor, with some filtering and optional delays.
 
@@ -1235,8 +1235,8 @@
 
   \item[Explicit completion] via action @{action_ref "isabelle.complete"}
   with keyboard shortcut @{verbatim "C+b"}. This overrides the shortcut for
-  @{verbatim "complete-word"} in jEdit. It is also possible to restore the
-  original jEdit keyboard mapping of @{verbatim "complete-word"} via
+  @{action_ref "complete-word"} in jEdit. It is also possible to restore the
+  original jEdit keyboard mapping of @{action "complete-word"} via
   \emph{Global Options / Shortcuts}, and invent a different one for @{action
   "isabelle.complete"}.
 
@@ -1344,9 +1344,9 @@
 
   \medskip Insertion works by removing and inserting pieces of text from the
   buffer. This counts as one atomic operation in terms of the jEdit
-  \emph{undo} history. Unintended completions may be reverted by the regular
-  @{verbatim undo} operation of jEdit. According to normal jEdit policies, the
-  recovered text after @{verbatim undo} is selected: @{verbatim ESCAPE} is
+  @{action_ref undo} history. Unintended completions may be reverted by the
+  regular @{action undo} action of jEdit. According to normal jEdit policies,
+  the recovered text after @{action undo} is selected: @{verbatim ESCAPE} is
   required to reset the selection and to to continue typing more text.
 *}
 
@@ -1658,7 +1658,7 @@
   \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
   "COMMAND+COMMA"} for application \emph{Preferences} is in conflict
   with the jEdit default shortcut for \emph{Incremental Search Bar}
-  (action @{verbatim "quick-search"}).
+  (action @{action_ref "quick-search"}).
 
   \textbf{Workaround:} Rebind key via \emph{Global Options /
   Shortcuts} according to national keyboard, e.g.\ @{verbatim
@@ -1690,7 +1690,7 @@
 
   \textbf{Workaround:} Use mainstream versions of Linux desktops.
 
-  \item \textbf{Problem:} Full-screen mode via jEdit action @{verbatim
+  \item \textbf{Problem:} Full-screen mode via jEdit action @{action_ref
   "toggle-full-screen"} (default shortcut @{verbatim F11}) works on
   Windows, but not on Mac OS X or various Linux / X11 window managers.
 
diff -r d58b7f7d81db -r 54c6b73774d2 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Mon Jun 16 20:50:56 2014 +0200
+++ b/src/Doc/antiquote_setup.ML	Mon Jun 16 21:26:50 2014 +0200
@@ -166,21 +166,32 @@
       | NONE => [])
   | parse_named _ _ = [];
 
-val jedit_actions =
+val isabelle_jedit_actions =
   (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
     XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
   | _ => []);
 
-val jedit_dockables =
+val isabelle_jedit_dockables =
   (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
     XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
   | _ => []);
 
-val all_actions = jedit_actions @ jedit_dockables;
+val jedit_actions =
+  Lazy.lazy (fn () =>
+    (case Isabelle_System.bash_output
+      "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
+      (txt, 0) =>
+        (case XML.parse txt of
+          XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
+        | _ => [])
+    | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
 
 in
 
-val is_action = member (op =) all_actions;
+fun is_action a =
+  member (op =) isabelle_jedit_actions a orelse
+  member (op =) isabelle_jedit_dockables a orelse
+  member (op =) (Lazy.force jedit_actions) a;
 
 end;