src/HOL/Library/code_test.ML
changeset 80328 559909bd7715
parent 78728 72631efa3821
child 81870 a4c0f9d12440
equal deleted inserted replaced
80327:e4e643705d90 80328:559909bd7715
   129   Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @
   129   Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @
   130     [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @
   130     [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @
   131     pretty_eval ctxt evals eval_ts)
   131     pretty_eval ctxt evals eval_ts)
   132 
   132 
   133 fun pretty_failures ctxt target failures =
   133 fun pretty_failures ctxt target failures =
   134   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   134   Pretty.block0 (Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   135 
   135 
   136 
   136 
   137 (* driver invocation *)
   137 (* driver invocation *)
   138 
   138 
   139 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)
   139 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)