src/Pure/Tools/codegen_serializer.ML

   end;
 
 fun parse_args f args =
   case Scan.read Args.stopper f args
    of SOME x => x
-    | NONE => error "bad serializer arguments";
+    | NONE => error "Bad serializer arguments";
 
 
 (* generic serializer combinators *)
 
 fun gen_pr_app pr_app' pr_term const_syntax vars fxy (app as ((c, (_, ty)), ts)) =

 
 val pretty_imperative_monad_bind =
   let
     fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T) vars fxy [t1, (v, ty) `|-> t2] =
           pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
-      | pretty _ _ _ _ = error "bad arguments for imperative monad bind";
+      | pretty _ _ _ _ = error "Bad arguments for imperative monad bind";
   in (2, pretty) end;
 
 
 
 (** name auxiliary **)

         val defname' =
           nodes
           |> fold (fn m => fn g => case Graph.get_node g m
               of Module (_, (_, g)) => g) modl'
           |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
-      in NameSpace.implode (remainder @ [defname']) end handle Graph.UNDEF _ =>
-        "(raise Fail \"undefined name " ^ name ^ "\")";
+      in
+        NameSpace.implode (remainder @ [defname'])
+      end handle Graph.UNDEF _ =>
+        error "Unknown name: " ^ quote name;
     fun the_prolog modlname = case module_prolog modlname
      of NONE => []
       | SOME p => [p, str ""];
     fun pr_node prefix (Def (_, NONE)) =
           NONE

 
 val isar_seri_sml =
   let
     fun output_file file = File.write (Path.explode file) o code_output;
     val output_diag = writeln o code_output;
-    val output_internal = use_text "" Output.ml_output false o code_output;
+    val output_internal = use_text "generated code" Output.ml_output false o code_output;
   in
     parse_args ((Args.$$$ "-" >> K output_diag
       || Args.$$$ "#" >> K output_internal
       || Args.name >> output_file)
     >> (fn output => seri_ml pr_sml pr_sml_modl output))

     val { class, inst, tyco, const } = the_syntax_expr data;
     fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;
     fun eval p = (
       reff := NONE;
       if !eval_verbose then Pretty.writeln p else ();
-      use_text "" Output.ml_output (!eval_verbose)
+      use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
         ((Pretty.output o Pretty.chunks) [p,
           str ("val _ = (" ^ ref_name ^ " := SOME " ^ val_name' ^ ")")
         ]);
       case !reff
        of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name