src/HOL/Spec_Check/output_style.ML
changeset 52253 afca6a99a361
parent 52252 81fcc11d8c65
child 52254 994055f7db80
equal deleted inserted replaced
52252:81fcc11d8c65 52253:afca6a99a361
    10 
    10 
    11 local
    11 local
    12 
    12 
    13 open StringCvt
    13 open StringCvt
    14 
    14 
    15 fun new ctxt tag =
    15 fun new context tag =
    16   let
    16   let
    17     val target = Config.get_generic ctxt Spec_Check.gen_target
    17     val target = Config.get_generic context Spec_Check.gen_target
    18     val namew = Config.get_generic ctxt Spec_Check.column_width
    18     val namew = Config.get_generic context Spec_Check.column_width
    19     val sort_examples = Config.get_generic ctxt Spec_Check.sort_examples
    19     val sort_examples = Config.get_generic context Spec_Check.sort_examples
    20     val show_stats = Config.get_generic ctxt Spec_Check.show_stats
    20     val show_stats = Config.get_generic context Spec_Check.show_stats
    21     val limit = Config.get_generic ctxt Spec_Check.examples
    21     val limit = Config.get_generic context Spec_Check.examples
    22 
    22 
    23     val resultw = 8
    23     val resultw = 8
    24     val countw = 20
    24     val countw = 20
    25     val allw = namew + resultw + countw + 2
    25     val allw = namew + resultw + countw + 2
    26 
    26 
    89 
    89 
    90 local
    90 local
    91 
    91 
    92 fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
    92 fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
    93 
    93 
    94 fun new ctxt tag =
    94 fun new context tag =
    95   let
    95   let
    96     val gen_target = Config.get_generic ctxt Spec_Check.gen_target
    96     val gen_target = Config.get_generic context Spec_Check.gen_target
    97     val _ = writeln ("[testing " ^ tag ^ "... ")
    97     val _ = writeln ("[testing " ^ tag ^ "... ")
    98     fun finish ({count, ...}, badobjs) =
    98     fun finish ({count, ...}, badobjs) =
    99       (case (count, badobjs) of
    99       (case (count, badobjs) of
   100         (0, []) => writeln ("no valid cases generated]")
   100         (0, []) => writeln ("no valid cases generated]")
   101       | (n, []) => writeln (
   101       | (n, []) => writeln (
   102             if n >= gen_target then "ok]"
   102             if n >= gen_target then "ok]"
   103             else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
   103             else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
   104       | (_, es) =>
   104       | (_, es) =>
   105         let
   105           let
   106           val wd = size (string_of_int (length es))
   106             val wd = size (string_of_int (length es))
   107           fun each (NONE, _) = ()
   107             fun each (NONE, _) = ()
   108             | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
   108               | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
   109          in
   109           in
   110            (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
   110             (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
   111          end)
   111           end)
   112   in
   112   in
   113     {status = K (), finish = finish}
   113     {status = K (), finish = finish}
   114   end
   114   end
   115 
   115 
   116 in
   116 in