src/HOL/Library/code_test.ML
changeset 64579 38a1d8b41189
parent 64578 7b20f9f94f4e
child 64580 43ad19fbe9dc
     1.1 --- a/src/HOL/Library/code_test.ML	Sat Dec 17 13:42:25 2016 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Sat Dec 17 14:04:05 2016 +0100
     1.3 @@ -228,7 +228,10 @@
     1.4      fun ensure_bool t =
     1.5        (case fastype_of t of
     1.6          @{typ bool} => ()
     1.7 -      | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t)))
     1.8 +      | _ =>
     1.9 +        error (Pretty.string_of
    1.10 +          (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1,
    1.11 +            Syntax.pretty_term ctxt t])))
    1.12  
    1.13      val _ = List.app ensure_bool ts
    1.14  
    1.15 @@ -253,32 +256,35 @@
    1.16  
    1.17  fun test_targets ctxt = List.app o test_terms ctxt
    1.18  
    1.19 +fun pretty_free ctxt = Syntax.pretty_term ctxt o Free
    1.20 +
    1.21  fun test_code_cmd raw_ts targets state =
    1.22    let
    1.23      val ctxt = Toplevel.context_of state
    1.24      val ts = Syntax.read_terms ctxt raw_ts
    1.25 -    val frees = fold Term.add_free_names ts []
    1.26 +    val frees = fold Term.add_frees ts []
    1.27      val _ =
    1.28        if null frees then ()
    1.29 -      else error ("Terms contain free variables: " ^
    1.30 -        Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
    1.31 +      else error (Pretty.string_of
    1.32 +        (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 ::
    1.33 +          Pretty.commas (map (pretty_free ctxt) frees))))
    1.34    in test_targets ctxt ts targets end
    1.35  
    1.36  fun eval_term target ctxt t =
    1.37    let
    1.38 -    val frees = Term.add_free_names t []
    1.39 +    val frees = Term.add_frees t []
    1.40      val _ =
    1.41        if null frees then ()
    1.42 -      else error ("Term contains free variables: " ^
    1.43 -        Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
    1.44 -
    1.45 -    val thy = Proof_Context.theory_of ctxt
    1.46 +      else
    1.47 +        error (Pretty.string_of
    1.48 +          (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 ::
    1.49 +            Pretty.commas (map (pretty_free ctxt) frees))))
    1.50  
    1.51 -    val T_t = fastype_of t
    1.52 +    val T = fastype_of t
    1.53      val _ =
    1.54 -      if Sign.of_sort thy (T_t, @{sort term_of}) then ()
    1.55 -      else error ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^
    1.56 -       " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
    1.57 +      if Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort term_of}) then ()
    1.58 +      else error ("Type " ^ Syntax.string_of_typ ctxt T ^
    1.59 +       " of term not of sort " ^ Syntax.string_of_sort ctxt @{sort term_of})
    1.60  
    1.61      val t' =
    1.62        HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
    1.63 @@ -297,7 +303,8 @@
    1.64        if compiler <> "" then ()
    1.65        else error (Pretty.string_of (Pretty.para
    1.66          ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
    1.67 -          compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
    1.68 +          compilerN ^ ", set this variable to your " ^ env_var_dest ^
    1.69 +          " in the $ISABELLE_HOME_USER/etc/settings file.")))
    1.70  
    1.71      fun compile NONE = ()
    1.72        | compile (SOME cmd) =