moved values command from core to predicate compile

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -155,6 +155,8 @@
 local structure P = OuterParse
 in
 
+(* Parser for mode annotations *)
+
 (*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*)
 datatype raw_argmode = Argmode of string | Argmode_Tuple of string list
 
@@ -185,16 +187,37 @@
   Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
     P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE
 
-val scan_params =
+(* Parser for options *)
+
+val scan_options =
   let
-    val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options)
+    val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
   in
-    Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") []
+    Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_option --| P.$$$ "]") []
   end
 
+val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val value_options =
+  let
+    val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
+    val random = Scan.optional (Args.$$$ "random" >> K true) false
+    val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false
+  in
+    Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]")
+      (NONE, (false, false))
+  end
+
+(* code_pred command and values command *)
+
 val _ = OuterSyntax.local_theory_to_proof "code_pred"
   "prove equations for predicate specified by intro/elim rules"
-  OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> code_pred_cmd)
+  OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
+  (opt_print_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
+    >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep
+        (Predicate_Compile_Core.values_cmd modes options k t)));
 
 end
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -6,9 +6,10 @@
 
 signature PREDICATE_COMPILE_CORE =
 sig
-  val setup: theory -> theory
-  val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
-  val code_pred_cmd: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+  val setup : theory -> theory
+  val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+  val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+  val values_cmd : string list -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
   val register_predicate : (string * thm list * thm * int) -> theory -> theory
   val register_intros : string * thm list -> theory -> theory
   val is_registered : theory -> string -> bool
@@ -23,13 +24,13 @@
   val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
   val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
   val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
-  val intros_of: theory -> string -> thm list
-  val nparams_of: theory -> string -> int
-  val add_intro: thm -> theory -> theory
-  val set_elim: thm -> theory -> theory
+  val intros_of : theory -> string -> thm list
+  val nparams_of : theory -> string -> int
+  val add_intro : thm -> theory -> theory
+  val set_elim : thm -> theory -> theory
   val set_nparams : string -> int -> theory -> theory
-  val print_stored_rules: theory -> unit
-  val print_all_modes: theory -> unit
+  val print_stored_rules : theory -> unit
+  val print_all_modes : theory -> unit
   val mk_casesrule : Proof.context -> term -> int -> thm list -> term
   val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
   val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref
@@ -2564,37 +2565,16 @@
   in
   end;
   *)
-fun values_cmd modes options k raw_t state =
+fun values_cmd print_modes options k raw_t state =
   let
     val ctxt = Toplevel.context_of state;
     val t = Syntax.read_term ctxt raw_t;
     val t' = values ctxt options k t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
+    val p = PrintMode.with_modes print_modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
 
-local structure P = OuterParse in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-val options =
-  let
-    val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
-    val random = Scan.optional (Args.$$$ "random" >> K true) false
-    val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false
-  in
-    Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]")
-      (NONE, (false, false))
-  end
-
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
-  (opt_modes -- options -- Scan.optional P.nat ~1 -- P.term
-    >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep
-        (values_cmd modes options k t)));
-
 end;
-
-end;