src/HOL/Library/code_test.ML
changeset 60022 ea987317a785
parent 59936 b8ffc3dc9e24
child 61077 06cca32aa519
equal deleted inserted replaced
60019:6e6cc8c012a2 60022:ea987317a785
   146          [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
   146          [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
   147           Syntax.pretty_term ctxt eval])
   147           Syntax.pretty_term ctxt eval])
   148        (ts ~~ evals))]
   148        (ts ~~ evals))]
   149 
   149 
   150 fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
   150 fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
   151   Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
   151   Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for")
       
   152     @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
   152     @ pretty_eval ctxt evals eval_ts)
   153     @ pretty_eval ctxt evals eval_ts)
   153 
   154 
   154 fun pretty_failures ctxt target failures =
   155 fun pretty_failures ctxt target failures =
   155   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   156   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   156 
   157