# HG changeset patch
# User wenzelm
# Date 1207832011 -7200
# Node ID 8a9d3eebd5344e3419234ae5ed95f5bbd4c95f8b
# Parent  1f09a22a1027b3902a9fdb24a4e962d7e55a3f5f
added read_const_exprs (from Pure/Isar/code_unit.ML);

diff -r 1f09a22a1027 -r 8a9d3eebd534 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Thu Apr 10 14:53:30 2008 +0200
+++ b/src/Tools/code/code_package.ML	Thu Apr 10 14:53:31 2008 +0200
@@ -144,6 +144,35 @@
 
 (* const expressions *)
 
+local
+
+fun consts_of thy some_thyname =
+  let
+    val this_thy = Option.map ThyInfo.get_theory some_thyname |> the_default thy;
+    val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
+    val cs = map (CodeUnit.subst_alias thy) raw_cs;
+    fun belongs_here thyname c =
+      not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
+  in case some_thyname
+   of NONE => cs
+    | SOME thyname => filter (belongs_here thyname) cs
+  end;
+
+fun read_const_expr thy "*" = ([], consts_of thy NONE)
+  | read_const_expr thy s = if String.isSuffix ".*" s
+      then ([], consts_of thy (SOME (unsuffix ".*" s)))
+      else ([CodeUnit.read_const thy s], []);
+
+in
+
+fun read_const_exprs thy select exprs =
+  case (pairself flat o split_list o map (read_const_expr thy)) exprs
+   of (consts, []) => (false, consts)
+    | (consts, consts') => (true, consts @ select consts');
+
+end; (*local*)
+
 fun filter_generatable thy consts =
   let
     val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
@@ -154,7 +183,7 @@
 
 fun generate_const_exprs thy raw_cs =
   let
-    val (perm1, cs) = CodeUnit.read_const_exprs thy
+    val (perm1, cs) = read_const_exprs thy
       (filter_generatable thy) raw_cs;
     val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs)
       (fold_map ooo ensure_const) cs
@@ -236,10 +265,10 @@
   in () end;
 
 fun code_thms_cmd thy =
-  code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
+  code_thms thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
 
 fun code_deps_cmd thy =
-  code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
+  code_deps thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
 
 fun code_props_cmd raw_cs seris thy =
   let