957 (Symbol.explode s) of |
957 (Symbol.explode s) of |
958 (p, []) => p |
958 (p, []) => p |
959 | _ => error ("Malformed annotation: " ^ quote s)); |
959 | _ => error ("Malformed annotation: " ^ quote s)); |
960 |
960 |
961 |
961 |
962 structure P = OuterParse and K = OuterKeyword; |
962 val _ = List.app Keyword.keyword ["attach", "file", "contains"]; |
963 |
|
964 val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"]; |
|
965 |
963 |
966 fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ") |
964 fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ") |
967 (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n"; |
965 (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n"; |
968 |
966 |
969 val parse_attach = Scan.repeat (P.$$$ "attach" |-- |
967 val parse_attach = Scan.repeat (Parse.$$$ "attach" |-- |
970 Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" -- |
968 Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" -- |
971 (P.verbatim >> strip_whitespace)); |
969 (Parse.verbatim >> strip_whitespace)); |
972 |
970 |
973 val _ = |
971 val _ = |
974 OuterSyntax.command "types_code" |
972 OuterSyntax.command "types_code" |
975 "associate types with target language types" K.thy_decl |
973 "associate types with target language types" Keyword.thy_decl |
976 (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> |
974 (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >> |
977 (fn xs => Toplevel.theory (fn thy => fold (assoc_type o |
975 (fn xs => Toplevel.theory (fn thy => fold (assoc_type o |
978 (fn ((name, mfx), aux) => (name, (parse_mixfix |
976 (fn ((name, mfx), aux) => (name, (parse_mixfix |
979 (Syntax.read_typ_global thy) mfx, aux)))) xs thy))); |
977 (Syntax.read_typ_global thy) mfx, aux)))) xs thy))); |
980 |
978 |
981 val _ = |
979 val _ = |
982 OuterSyntax.command "consts_code" |
980 OuterSyntax.command "consts_code" |
983 "associate constants with target language code" K.thy_decl |
981 "associate constants with target language code" Keyword.thy_decl |
984 (Scan.repeat1 |
982 (Scan.repeat1 |
985 (P.term --| |
983 (Parse.term --| |
986 P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> |
984 Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >> |
987 (fn xs => Toplevel.theory (fn thy => fold (assoc_const o |
985 (fn xs => Toplevel.theory (fn thy => fold (assoc_const o |
988 (fn ((const, mfx), aux) => |
986 (fn ((const, mfx), aux) => |
989 (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy))); |
987 (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy))); |
990 |
988 |
991 fun parse_code lib = |
989 fun parse_code lib = |
992 Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) -- |
990 Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") (!mode) -- |
993 (if lib then Scan.optional P.name "" else P.name) -- |
991 (if lib then Scan.optional Parse.name "" else Parse.name) -- |
994 Scan.option (P.$$$ "file" |-- P.name) -- |
992 Scan.option (Parse.$$$ "file" |-- Parse.name) -- |
995 (if lib then Scan.succeed [] |
993 (if lib then Scan.succeed [] |
996 else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --| |
994 else Scan.optional (Parse.$$$ "imports" |-- Scan.repeat1 Parse.name) []) --| |
997 P.$$$ "contains" -- |
995 Parse.$$$ "contains" -- |
998 ( Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) |
996 ( Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term) |
999 || Scan.repeat1 (P.term >> pair "")) >> |
997 || Scan.repeat1 (Parse.term >> pair "")) >> |
1000 (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => |
998 (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => |
1001 let |
999 let |
1002 val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode'); |
1000 val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode'); |
1003 val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs; |
1001 val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs; |
1004 val thy' = thy |> Context.theory_map (ML_Context.exec (fn () => |
1002 val thy' = thy |> Context.theory_map (ML_Context.exec (fn () => |