src/Tools/code/code_target.ML

   val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;
 
   type serializer;
   val add_serializer: string * serializer -> theory -> theory;
   val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
-    -> (theory -> string -> string) -> string list option -> CodeThingol.code -> unit;
+    -> (theory -> string -> string) -> (string -> bool) -> string list option
+    -> CodeThingol.code -> unit;
   val assert_serializer: theory -> string -> string;
 
   val eval_verbose: bool ref;
-  val eval_term: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
-    ->  CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
+  val eval_invoke: theory -> (theory -> string -> string) -> (string -> bool)
+    -> (string * (unit -> 'a) option ref) -> CodeThingol.code
+    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
   val code_width: int ref;
 
   val setup: theory -> theory;
 end;
 

   | MLClass of string * ((class * string) list * (vname * (string * itype) list))
   | MLClassinst of string * ((class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
       * (string * const) list));
 
-fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
+fun pr_sml allows_exception tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
   let
     val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
     val pr_label_classop = NameSpace.base o NameSpace.qualifier;
     fun pr_dicts fxy ds =
       let

   ] @ content @ [
     str "",
     str ("end; (*struct " ^ name ^ "*)")
   ]);
 
-fun pr_ocaml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
+fun pr_ocaml allows_exception tyco_syntax const_syntax labelled_name
+    init_syms deresolv is_cons ml_def =
   let
     fun pr_dicts fxy ds =
       let
         fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
           | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);

 
 val code_width = ref 80;
 fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
 
 fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog
-  (_ : string -> class_syntax option) tyco_syntax const_syntax code =
+  allows_exception (_ : string -> class_syntax option) tyco_syntax const_syntax code =
   let
     val module_alias = if is_some module then K module else raw_module_alias;
     val is_cons = CodeThingol.is_cons code;
     datatype node =
         Def of string * ml_def option

      of NONE => []
       | SOME p => [p, str ""];
     fun pr_node prefix (Def (_, NONE)) =
           NONE
       | pr_node prefix (Def (_, SOME def)) =
-          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
+          SOME (pr_def allows_exception tyco_syntax const_syntax labelled_name init_syms
             (deresolver prefix) is_cons def)
       | pr_node prefix (Module (dmodlname, (_, nodes))) =
           SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
             @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
                 o rev o flat o Graph.strong_conn) nodes)));

 
 val pr_bind_haskell = gen_pr_bind pr_bind';
 
 in
 
-fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
-    deresolv_here deresolv is_cons deriving_show def =
+fun pr_haskell allows_exception class_syntax tyco_syntax const_syntax labelled_name
+    init_syms deresolv_here deresolv is_cons deriving_show def =
   let
     fun class_name class = case class_syntax class
      of NONE => deresolv class
       | SOME (class, _) => class;
     fun classop_name class classop = case class_syntax class

   in (1, pretty) end;
 
 end; (*local*)
 
 fun seri_haskell module_prefix module destination string_classes labelled_name
-    reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
+    reserved_syms raw_module_alias module_prolog
+    allows_exception class_syntax tyco_syntax const_syntax code =
   let
     val _ = Option.map File.check destination;
     val is_cons = CodeThingol.is_cons code;
     val module_alias = if is_some module then K module else raw_module_alias;
     val init_names = Name.make_context reserved_syms;

                     (maps snd cs)
         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
               andalso forall (deriv' tycos) tys
           | deriv' _ (ITyVar _) = true
       in deriv [] tyco end;
-    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
+    fun seri_def qualified = pr_haskell allows_exception class_syntax tyco_syntax
+      const_syntax labelled_name init_syms
       deresolv_here (if qualified then deresolv else deresolv_here) is_cons
       (if string_classes then deriving_show else K false);
     fun write_module (SOME destination) modlname =
           let
             val filename = case modlname

   end;
 
 
 (** diagnosis serializer **)
 
-fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
+fun seri_diagnosis labelled_name _ _ _ _ _ _ _ code =
   let
     val init_names = CodeName.make_vars [];
     fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
           brackify_infix (1, R) fxy [
             pr_typ (INFX (1, X)) ty1,
             str "->",
             pr_typ (INFX (1, R)) ty2
           ])
       | pr_fun _ = NONE
-    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
+    val pr = pr_haskell (K true) (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
   in
     []
     |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
     |> Pretty.chunks2
     |> code_output

   -> Args.T list
   -> (string -> string)
   -> string list
   -> (string -> string option)
   -> (string -> Pretty.T option)
+  -> (string -> bool)
   -> (string -> class_syntax option)
   -> (string -> typ_syntax option)
   -> (string -> term_syntax option)
   -> CodeThingol.code -> unit;
 

 val target_SML = "SML";
 val target_OCaml = "OCaml";
 val target_Haskell = "Haskell";
 val target_diag = "diag";
 
-fun get_serializer thy target permissive module file args labelled_name = fn cs =>
+fun get_serializer thy target permissive module file args
+    labelled_name allows_exception = fn cs =>
   let
     val data = case Symtab.lookup (CodeTargetData.get thy) target
      of SOME data => data
       | NONE => error ("Unknown code target language: " ^ quote target);
     val seri = the_serializer data;

       | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
   in
     project
     #> check_empty_funs
     #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
-      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
-  end;
-
-fun eval_term thy (ref_name, reff) code (t, ty) args =
+      allows_exception (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
+  end;
+
+fun eval_invoke thy labelled_name allows_exception (ref_name, reff) code (t, ty) args =
   let
     val val_name = "Isabelle_Eval.EVAL.EVAL";
     val val_name' = "Isabelle_Eval.EVAL";
     val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
-    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] CodeName.labelled_name;
+    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
+      labelled_name allows_exception;
     fun eval code = (
       reff := NONE;
       seri (SOME [val_name]) code;
       use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
         ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_name'_args ^ "))");