src/HOL/Library/code_test.ML
changeset 72293 584aea0b29bb
parent 72291 ccc104786829
child 72296 00490c408e52
equal deleted inserted replaced
72292:4a58c38b85ff 72293:584aea0b29bb
   139   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   139   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   140 
   140 
   141 
   141 
   142 (* driver invocation *)
   142 (* driver invocation *)
   143 
   143 
   144 val debug = Attrib.setup_config_bool \<^binding>\<open>code_test_debug\<close> (K false)
   144 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)
   145 
   145 
   146 fun with_debug_dir name f =
   146 fun with_debug_dir name f =
   147   let
   147   let
   148     val dir =
   148     val dir =
   149       Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
   149       Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))