src/Tools/Code/code_target.ML

   val add_syntax_class: string -> class -> string option -> theory -> theory
   val add_syntax_inst: string -> string * class -> bool -> theory -> theory
   val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
   val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
+  val add_include: string -> string * (string * string list) option -> theory -> theory
 end;
 
 structure Code_Target : CODE_TARGET =
 struct
 

 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
 fun the_module_alias (Target { module_alias , ... }) = module_alias;
 
 val abort_allowed = snd o CodeTargetData.get;
 
-fun assert_target thy target =
-  case Symtab.lookup (fst (CodeTargetData.get thy)) target
-   of SOME data => target
-    | NONE => error ("Unknown code target language: " ^ quote target);
+fun assert_target thy target = if Symtab.defined (fst (CodeTargetData.get thy)) target
+  then target
+  else error ("Unknown code target language: " ^ quote target);
 
 fun put_target (target, seri) thy =
   let
     val lookup_target = Symtab.lookup (fst (CodeTargetData.get thy));
     val _ = case seri

       else error ("No such type constructor: " ^ quote tyco);
   in tyco end;
 
 fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
 
-fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
+fun gen_add_syntax_class prep_class target raw_class raw_syn thy =
   let
     val class = prep_class thy raw_class;
   in case raw_syn
    of SOME syntax =>
       thy

             val cs = map (read_const thy) raw_cs;
           in Symtab.update (name, (str content, cs)) incls end
       | add (name, NONE) incls = Symtab.delete name incls;
   in map_includes target (add args) thy end;
 
-val add_include = gen_add_include Code.check_const;
+val add_include = gen_add_include (K I);
 val add_include_cmd = gen_add_include Code.read_const;
 
 fun add_module_alias target (thyname, modlname) =
   let
     val xs = Long_Name.explode modlname;

   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
 
 in
 
-val add_syntax_class = gen_add_syntax_class cert_class (K I);
+val add_syntax_class = gen_add_syntax_class cert_class;
 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
 val add_syntax_const = gen_add_syntax_const (K I);
 val allow_abort = gen_allow_abort (K I);
 val add_reserved = add_reserved;
-
-val add_syntax_class_cmd = gen_add_syntax_class read_class Code.read_const;
+val add_include = add_include;
+
+val add_syntax_class_cmd = gen_add_syntax_class read_class;
 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
 val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
 val allow_abort_cmd = gen_allow_abort Code.read_const;
 

 fun shell_command thyname cmd = Toplevel.program (fn _ =>
   (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
     ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
    of SOME f => (writeln "Now generating code..."; f (theory thyname))
     | NONE => error ("Bad directive " ^ quote cmd)))
-  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
+  handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 
 end; (*local*)
 
 end; (*struct*)