# HG changeset patch
# User haftmann
# Date 1412866076 -7200
# Node ID 133203bd474bdad1adcdef0ffeaa308703a5fc51
# Parent  8d108c0e7da240ba7634948f9cfbb846a5ed0c3d
formally completeted set of experimental static evaluation functions

diff -r 8d108c0e7da2 -r 133203bd474b src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Oct 09 17:31:50 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Oct 09 16:47:56 2014 +0200
@@ -28,6 +28,14 @@
     -> Proof.context -> term -> 'a Exn.result
   val dynamic_holds_conv: Proof.context -> conv
   val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
+  val static_value': (Proof.context -> term -> 'a) cookie
+    -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
+           consts: (string * typ) list, T: typ }
+    -> Proof.context -> term -> 'a option (*EXPERIMENTAL!*)
+  val static_value_strict': (Proof.context -> term -> 'a) cookie
+    -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
+           consts: (string * typ) list, T: typ }
+    -> Proof.context -> term -> 'a (*EXPERIMENTAL!*)
   val static_value_exn': (Proof.context -> term -> 'a) cookie
     -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
            consts: (string * typ) list, T: typ }
@@ -311,6 +319,10 @@
     evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
   end;
 
+fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie;
+
+fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
+
 
 (** code antiquotation **)