equal
deleted
inserted
replaced
138 (* driver invocation *) |
138 (* driver invocation *) |
139 |
139 |
140 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false) |
140 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false) |
141 |
141 |
142 fun with_debug_dir name f = |
142 fun with_debug_dir name f = |
143 let |
143 Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) |
144 val dir = |
144 |> Isabelle_System.make_directory |
145 Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) |
145 |> Exn.capture f |
146 val _ = Isabelle_System.make_directory dir |
146 |> Exn.release; |
147 in Exn.release (Exn.capture f dir) end |
|
148 |
147 |
149 fun dynamic_value_strict ctxt t compiler = |
148 fun dynamic_value_strict ctxt t compiler = |
150 let |
149 let |
151 val thy = Proof_Context.theory_of ctxt |
150 val thy = Proof_Context.theory_of ctxt |
152 val (driver, target) = |
151 val (driver, target) = |