src/Tools/Code/code_ml.ML
changeset 59323 468bd3aedfa1
parent 59104 a14475f044b2
child 59456 180555df34ea
equal deleted inserted replaced
59322:8ccecf1415b0 59323:468bd3aedfa1
     6 
     6 
     7 signature CODE_ML =
     7 signature CODE_ML =
     8 sig
     8 sig
     9   val target_SML: string
     9   val target_SML: string
    10   val target_OCaml: string
    10   val target_OCaml: string
    11   val setup: theory -> theory
       
    12 end;
    11 end;
    13 
    12 
    14 structure Code_ML : CODE_ML =
    13 structure Code_ML : CODE_ML =
    15 struct
    14 struct
    16 
    15 
   858     print_typ (INFX (1, X)) ty1,
   857     print_typ (INFX (1, X)) ty1,
   859     str "->",
   858     str "->",
   860     print_typ (INFX (1, R)) ty2
   859     print_typ (INFX (1, R)) ty2
   861   );
   860   );
   862 
   861 
   863 val setup =
   862 val _ = Theory.setup
   864   Code_Target.add_language
   863   (Code_Target.add_language
   865     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   864     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   866       check = { env_var = "ISABELLE_PROCESS",
   865       check = { env_var = "ISABELLE_PROCESS",
   867         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   866         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   868         make_command = fn _ =>
   867         make_command = fn _ =>
   869           "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
   868           "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
   885       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   884       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   886       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   885       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   887       "sig", "struct", "then", "to", "true", "try", "type", "val",
   886       "sig", "struct", "then", "to", "true", "try", "type", "val",
   888       "virtual", "when", "while", "with"
   887       "virtual", "when", "while", "with"
   889     ]
   888     ]
   890   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
   889   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]);
   891 
   890 
   892 end; (*struct*)
   891 end; (*struct*)