# HG changeset patch
# User wenzelm
# Date 1447182617 -3600
# Node ID cd7549cd5fe7d7a76c26b7e7b7f107bd765001a3
# Parent  abbecf4e660175d66100b34b1be32bff7c0a1328
clarified modules;

diff -r abbecf4e6601 -r cd7549cd5fe7 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Tue Nov 10 19:56:51 2015 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Nov 10 20:10:17 2015 +0100
@@ -141,46 +141,6 @@
             #> enclose "\\isa{" "}")));
 
 
-(* Isabelle/jEdit elements *)
-
-local
-
-fun parse_named a (XML.Elem ((b, props), _)) =
-      (case Properties.get props "NAME" of
-        SOME name => if a = b then [name] else []
-      | NONE => [])
-  | parse_named _ _ = [];
-
-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 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 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
-
-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;
-
-
 (* Isabelle/Isar entities (with index) *)
 
 local
@@ -275,7 +235,7 @@
     entity_antiqs no_check "isasystem" @{binding executable} #>
     entity_antiqs check_tool "isatool" @{binding tool} #>
     entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
-    entity_antiqs (K (is_action o #1)) "isasystem" @{binding action});
+    entity_antiqs (K (JEdit.is_action o #1)) "isasystem" @{binding action});
 
 end;
 
diff -r abbecf4e6601 -r cd7549cd5fe7 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Nov 10 19:56:51 2015 +0100
+++ b/src/Pure/Pure.thy	Tue Nov 10 20:10:17 2015 +0100
@@ -109,6 +109,7 @@
 ML_file "Tools/simplifier_trace.ML"
 ML_file "Tools/debugger.ML"
 ML_file "Tools/named_theorems.ML"
+ML_file "Tools/jedit.ML"
 
 
 section \<open>Basic attributes\<close>
@@ -298,4 +299,3 @@
 qed
 
 end
-
diff -r abbecf4e6601 -r cd7549cd5fe7 src/Pure/Tools/jedit.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/jedit.ML	Tue Nov 10 20:10:17 2015 +0100
@@ -0,0 +1,56 @@
+(*  Title:      Pure/Tools/jedit.ML
+    Author:     Makarius
+
+jEdit support.
+*)
+
+signature JEDIT =
+sig
+  val is_action: string -> bool
+end;
+
+structure JEdit: JEDIT =
+struct
+
+(* jEdit actions *)
+
+local
+
+fun parse_named a (XML.Elem ((b, props), _)) =
+      (case Properties.get props "NAME" of
+        SOME name => if a = b then [name] else []
+      | NONE => [])
+  | parse_named _ _ = [];
+
+val isabelle_jedit_actions =
+  Lazy.lazy (fn () =>
+    (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
+      XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
+    | _ => []));
+
+val isabelle_jedit_dockables =
+  Lazy.lazy (fn () =>
+    (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
+      XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
+    | _ => []));
+
+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
+
+fun is_action a =
+  member (op =) (Lazy.force isabelle_jedit_actions) a orelse
+  member (op =) (Lazy.force isabelle_jedit_dockables) a orelse
+  member (op =) (Lazy.force jedit_actions) a;
+
+end;
+
+end;