# HG changeset patch
# User wenzelm
# Date 1481979845 -3600
# Node ID 38a1d8b411891866b2b244256075a466961bac07
# Parent  7b20f9f94f4e2e5cfb044be4f4e6894e65e01ffb
more standard pretty printing;
tuned messages;

diff -r 7b20f9f94f4e -r 38a1d8b41189 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Sat Dec 17 13:42:25 2016 +0100
+++ b/src/HOL/Library/code_test.ML	Sat Dec 17 14:04:05 2016 +0100
@@ -228,7 +228,10 @@
     fun ensure_bool t =
       (case fastype_of t of
         @{typ bool} => ()
-      | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t)))
+      | _ =>
+        error (Pretty.string_of
+          (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1,
+            Syntax.pretty_term ctxt t])))
 
     val _ = List.app ensure_bool ts
 
@@ -253,32 +256,35 @@
 
 fun test_targets ctxt = List.app o test_terms ctxt
 
+fun pretty_free ctxt = Syntax.pretty_term ctxt o Free
+
 fun test_code_cmd raw_ts targets state =
   let
     val ctxt = Toplevel.context_of state
     val ts = Syntax.read_terms ctxt raw_ts
-    val frees = fold Term.add_free_names ts []
+    val frees = fold Term.add_frees ts []
     val _ =
       if null frees then ()
-      else error ("Terms contain free variables: " ^
-        Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
+      else error (Pretty.string_of
+        (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 ::
+          Pretty.commas (map (pretty_free ctxt) frees))))
   in test_targets ctxt ts targets end
 
 fun eval_term target ctxt t =
   let
-    val frees = Term.add_free_names t []
+    val frees = Term.add_frees t []
     val _ =
       if null frees then ()
-      else error ("Term contains free variables: " ^
-        Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
-
-    val thy = Proof_Context.theory_of ctxt
+      else
+        error (Pretty.string_of
+          (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 ::
+            Pretty.commas (map (pretty_free ctxt) frees))))
 
-    val T_t = fastype_of t
+    val T = fastype_of t
     val _ =
-      if Sign.of_sort thy (T_t, @{sort term_of}) then ()
-      else error ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^
-       " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
+      if Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort term_of}) then ()
+      else error ("Type " ^ Syntax.string_of_typ ctxt T ^
+       " of term not of sort " ^ Syntax.string_of_sort ctxt @{sort term_of})
 
     val t' =
       HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
@@ -297,7 +303,8 @@
       if compiler <> "" then ()
       else error (Pretty.string_of (Pretty.para
         ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
-          compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
+          compilerN ^ ", set this variable to your " ^ env_var_dest ^
+          " in the $ISABELLE_HOME_USER/etc/settings file.")))
 
     fun compile NONE = ()
       | compile (SOME cmd) =