# HG changeset patch # User haftmann # Date 1279533344 -7200 # Node ID 096c8397c989081be4b780edb71cba6620a8c765 # Parent 3b9ca8d2c5fbbbf01056036f5ede40e43508bc8b distinguish different classes of const syntax diff -r 3b9ca8d2c5fb -r 096c8397c989 src/HOL/Tools/list_code.ML --- a/src/HOL/Tools/list_code.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/HOL/Tools/list_code.ML Mon Jul 19 11:55:44 2010 +0200 @@ -46,8 +46,8 @@ Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts) | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; - in Code_Target.add_syntax_const target - @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty))) + in Code_Target.add_syntax_const target @{const_name Cons} + (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))) end end; diff -r 3b9ca8d2c5fb -r 096c8397c989 src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/HOL/Tools/numeral.ML Mon Jul 19 11:55:44 2010 +0200 @@ -77,8 +77,8 @@ (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t; in thy |> Code_Target.add_syntax_const target number_of - (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, - @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))) + (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, + @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))) end; end; (*local*) diff -r 3b9ca8d2c5fb -r 096c8397c989 src/HOL/Tools/string_code.ML --- a/src/HOL/Tools/string_code.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/HOL/Tools/string_code.ML Mon Jul 19 11:55:44 2010 +0200 @@ -60,7 +60,7 @@ | NONE => List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; in Code_Target.add_syntax_const target - @{const_name Cons} (SOME (2, (cs_summa, pretty))) + @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty)))) end; fun add_literal_char target = @@ -70,7 +70,7 @@ of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c | NONE => Code_Printer.eqn_error thm "Illegal character expression"; in Code_Target.add_syntax_const target - @{const_name Char} (SOME (2, (cs_nibbles, pretty))) + @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty)))) end; fun add_literal_string target = @@ -83,7 +83,7 @@ | NONE => Code_Printer.eqn_error thm "Illegal message expression") | NONE => Code_Printer.eqn_error thm "Illegal message expression"; in Code_Target.add_syntax_const target - @{const_name STR} (SOME (1, (cs_summa, pretty))) + @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty)))) end; end; diff -r 3b9ca8d2c5fb -r 096c8397c989 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Mon Jul 19 11:55:44 2010 +0200 @@ -218,30 +218,35 @@ | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) = let val tyvars = intro_vars (map fst vs) reserved; - fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam - of NONE => semicolon [ - (str o deresolve_base) classparam, - str "=", - print_app tyvars (SOME thm) reserved NOBR (const, []) - ] - | SOME (k, pr) => - let - val (c, (_, tys)) = const; - val (vs, rhs) = (apfst o map) fst - (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); - val s = if (is_some o syntax_const) c - then NONE else (SOME o Long_Name.base_name o deresolve) c; - val vars = reserved - |> intro_vars (map_filter I (s :: vs)); - val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; - (*dictionaries are not relevant at this late stage*) - in - semicolon [ - print_term tyvars (SOME thm) vars NOBR lhs, + fun requires_args classparam = case syntax_const classparam + of NONE => 0 + | SOME (Code_Printer.Plain_const_syntax _) => 0 + | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k; + fun print_classparam_instance ((classparam, const), (thm, _)) = + case requires_args classparam + of 0 => semicolon [ + (str o deresolve_base) classparam, str "=", - print_term tyvars (SOME thm) vars NOBR rhs + print_app tyvars (SOME thm) reserved NOBR (const, []) ] - end; + | k => + let + val (c, (_, tys)) = const; + val (vs, rhs) = (apfst o map) fst + (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); + val s = if (is_some o syntax_const) c + then NONE else (SOME o Long_Name.base_name o deresolve) c; + val vars = reserved + |> intro_vars (map_filter I (s :: vs)); + val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; + (*dictionaries are not relevant at this late stage*) + in + semicolon [ + print_term tyvars (SOME thm) vars NOBR lhs, + str "=", + print_term tyvars (SOME thm) vars NOBR rhs + ] + end; in Pretty.block_enclose ( Pretty.block [ @@ -459,7 +464,7 @@ in if target = target' then thy |> Code_Target.add_syntax_const target c_bind - (SOME (pretty_haskell_monad c_bind)) + (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind))) else error "Only Haskell target allows for monad syntax" end; diff -r 3b9ca8d2c5fb -r 096c8397c989 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/Tools/Code/code_printer.ML Mon Jul 19 11:55:44 2010 +0200 @@ -67,17 +67,19 @@ type tyco_syntax type simple_const_syntax + type complex_const_syntax type const_syntax - type activated_const_syntax - val parse_infix: ('a -> 'b) -> lrx * int -> string - -> int * ((fixity -> 'b -> Pretty.T) - -> fixity -> 'a list -> Pretty.T) - val parse_syntax: ('a -> 'b) -> Token.T list - -> (int * ((fixity -> 'b -> Pretty.T) - -> fixity -> 'a list -> Pretty.T)) option * Token.T list + type activated_complex_const_syntax + datatype activated_const_syntax = Plain_const_syntax of int * string + | Complex_const_syntax of activated_complex_const_syntax + val requires_args: const_syntax -> int + val parse_const_syntax: Token.T list -> const_syntax option * Token.T list + val parse_tyco_syntax: Token.T list -> tyco_syntax option * Token.T list + val plain_const_syntax: string -> const_syntax val simple_const_syntax: simple_const_syntax -> const_syntax + val complex_const_syntax: complex_const_syntax -> const_syntax val activate_const_syntax: theory -> literals - -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming + -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list) -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) -> (string -> activated_const_syntax option) @@ -243,31 +245,45 @@ type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T) -> fixity -> (iterm * itype) list -> Pretty.T); -type const_syntax = int * (string list * (literals -> string list + +type complex_const_syntax = int * (string list * (literals -> string list -> (var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)); -type activated_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T) - -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); + +datatype const_syntax = plain_const_syntax of string + | complex_const_syntax of complex_const_syntax; + +fun requires_args (plain_const_syntax _) = 0 + | requires_args (complex_const_syntax (k, _)) = k; fun simple_const_syntax syn = - apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn; + complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn); -fun activate_const_syntax thy literals (n, (cs, f)) naming = - fold_map (Code_Thingol.ensure_declared_const thy) cs naming - |-> (fn cs' => pair (n, f literals cs')); +type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T) + -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T) + +datatype activated_const_syntax = Plain_const_syntax of int * string + | Complex_const_syntax of activated_complex_const_syntax; -fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) = +fun activate_const_syntax thy literals c (plain_const_syntax s) naming = + (Plain_const_syntax (Code.args_number thy c, s), naming) + | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming = + fold_map (Code_Thingol.ensure_declared_const thy) cs naming + |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs'))); + +fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) = case syntax_const c - of NONE => brackify fxy (print_app_expr thm vars app) - | SOME (k, print) => + of NONE => brackify fxy (print_app_expr some_thm vars app) + | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts) + | SOME (Complex_const_syntax (k, print)) => let - fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs); + fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs); in if k = length ts then print' fxy ts else if k < length ts then case chop k ts of (ts1, ts2) => - brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2) - else print_term thm vars fxy (Code_Thingol.eta_expand k app) + brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) + else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) end; fun gen_print_bind print_term thm (fxy : fixity) pat vars = @@ -281,7 +297,8 @@ datatype 'a mixfix = Arg of fixity - | Pretty of Pretty.T; + | String of string + | Break; fun mk_mixfix prep_arg (fixity_this, mfx) = let @@ -292,8 +309,10 @@ [] | fillin print (Arg fxy :: mfx) (a :: args) = (print fxy o prep_arg) a :: fillin print mfx args - | fillin print (Pretty p :: mfx) args = - p :: fillin print mfx args; + | fillin print (String s :: mfx) args = + str s :: fillin print mfx args + | fillin print (Break :: mfx) args = + Pretty.brk 1 :: fillin print mfx args; in (i, fn print => fn fixity_ctxt => fn args => gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args)) @@ -304,42 +323,45 @@ val l = case x of L => INFX (i, L) | _ => INFX (i, X); val r = case x of R => INFX (i, R) | _ => INFX (i, X); in - mk_mixfix prep_arg (INFX (i, x), - [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]) + mk_mixfix prep_arg (INFX (i, x), [Arg l, String " ", String s, Break, Arg r]) end; -fun parse_mixfix prep_arg s = +fun parse_mixfix mk_plain mk_complex prep_arg s = let val sym_any = Scan.one Symbol.is_regular; val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat ( ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) || ($$ "_" >> K (Arg BR)) - || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)) + || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break)) || (Scan.repeat1 ( $$ "'" |-- sym_any || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") - sym_any) >> (Pretty o str o implode))); + sym_any) >> (String o implode))); in case Scan.finite Symbol.stopper parse (Symbol.explode s) - of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p) - | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p) + of ((false, [String s]), []) => mk_plain s + | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p)) + | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p)) | _ => Scan.!! (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail () end; val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr"); -fun parse_syntax prep_arg xs = - Scan.option (( +fun parse_syntax mk_plain mk_complex prep_arg = + Scan.option ( ((Parse.$$$ infixK >> K X) || (Parse.$$$ infixlK >> K L) || (Parse.$$$ infixrK >> K R)) - -- Parse.nat >> parse_infix prep_arg - || Scan.succeed (parse_mixfix prep_arg)) - -- Parse.string - >> (fn (parse, s) => parse s)) xs; + -- Parse.nat -- Parse.string + >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s)) + || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s))); val _ = List.app Keyword.keyword [infixK, infixlK, infixrK]; +val parse_tyco_syntax = parse_syntax (fn s => (0, (K o K o K o str) s)) I I; + +val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst; + (** module name spaces **) diff -r 3b9ca8d2c5fb -r 096c8397c989 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Mon Jul 19 11:55:44 2010 +0200 @@ -76,17 +76,20 @@ (app as ((c, ((arg_typs, _), function_typs)), ts)) = let val k = length ts; - val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l; val arg_typs' = if is_pat orelse (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs; - val (no_syntax, print') = case syntax_const c - of NONE => (true, fn ts => applify "(" ")" + val (l, print') = case syntax_const c + of NONE => (args_num c, fn ts => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) NOBR ((str o deresolve) c) arg_typs') ts) - | SOME (_, print) => (false, fn ts => - print (print_term tyvars is_pat some_thm) some_thm vars fxy - (ts ~~ take l function_typs)); + | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")" + (print_term tyvars is_pat some_thm vars NOBR) fxy + (applify "[" "]" (print_typ tyvars NOBR) + NOBR (str s) arg_typs') ts) + | SOME (Complex_const_syntax (k, print)) => + (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy + (ts ~~ take k function_typs)) in if k = l then print' ts else if k < l then print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app) @@ -355,20 +358,22 @@ | _ => false; val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton_constr deresolver; - fun print_module name content = - (name, Pretty.chunks [ - str ("object " ^ name ^ " {"), - str "", + fun print_module name imports content = + (name, Pretty.chunks ( + str ("object " ^ name ^ " {") + :: (if null imports then [] + else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports) + @ [str "", content, str "", - str "}" - ]); + str "}"] + )); fun serialize_module the_module_name sca_program = let val content = Pretty.chunks2 (map_filter (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt)) | (_, (_, NONE)) => NONE) sca_program); - in print_module the_module_name content end; + in print_module the_module_name (map fst includes) content end; fun check_destination destination = (File.check destination; destination); fun write_module destination (modlname, content) = @@ -385,7 +390,7 @@ (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map (write_module (check_destination file))) (rpair [] o cat_lines o map (code_of_pretty o snd)) - (map (uncurry print_module) includes + (map (fn (name, content) => print_module name [] content) includes @| serialize_module the_module_name sca_program) destination end; @@ -405,7 +410,7 @@ literal_char = Library.enclose "'" "'" o char_scala, literal_string = quote o translate_string char_scala, literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")", - literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")", + literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")", literal_naive_numeral = fn k => if k >= 0 then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")", literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps], diff -r 3b9ca8d2c5fb -r 096c8397c989 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/Tools/Code/code_target.ML Mon Jul 19 11:55:44 2010 +0200 @@ -244,11 +244,11 @@ |>> map_filter I; fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming) - |> fold_map (fn thing_identifier => fn (tab, naming) => - case Code_Thingol.lookup_const naming thing_identifier + |> fold_map (fn c => fn (tab, naming) => + case Code_Thingol.lookup_const naming c of SOME name => let val (syn, naming') = Code_Printer.activate_const_syntax thy - literals (the (Symtab.lookup src_tab thing_identifier)) naming + literals c (the (Symtab.lookup src_tab c)) naming in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab) |>> map_filter I; @@ -445,12 +445,12 @@ then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco) else syn); -fun gen_add_syntax_const prep_const prep_syn = +fun gen_add_syntax_const prep_const = gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const - (fn thy => fn c => fn raw_syn => let val syn = prep_syn raw_syn in - if fst syn > Code.args_number thy c + (fn thy => fn c => fn syn => + if Code_Printer.requires_args syn > Code.args_number thy c then error ("Too many arguments in syntax for constant " ^ quote c) - else syn end); + else syn); fun add_reserved target = let @@ -496,22 +496,23 @@ fun zip_list (x::xs) f g = f - #-> (fn y => + :|-- (fn y => fold_map (fn x => g |-- f >> pair x) xs - #-> (fn xys => pair ((x, y) :: xys))); + :|-- (fn xys => pair ((x, y) :: xys))); -fun parse_multi_syntax parse_thing parse_syntax = - Parse.and_list1 parse_thing - #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name -- - (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")); +fun process_multi_syntax parse_thing parse_syntax change = + (Parse.and_list1 parse_thing + :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name -- + (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"))) + >> (Toplevel.theory oo fold) + (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns); in val add_syntax_class = gen_add_syntax_class cert_class; val add_syntax_inst = gen_add_syntax_inst cert_inst; val add_syntax_tyco = gen_add_syntax_tyco cert_tyco; -val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax; -val add_syntax_const = gen_add_syntax_const (K I) I; +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_include = add_include; @@ -519,9 +520,7 @@ val add_syntax_class_cmd = gen_add_syntax_class read_class; val add_syntax_inst_cmd = gen_add_syntax_inst read_inst; val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco; -val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax; -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I; - +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const; val allow_abort_cmd = gen_allow_abort Code.read_const; fun parse_args f args = @@ -550,32 +549,24 @@ val _ = Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl ( - parse_multi_syntax Parse.xname (Scan.option Parse.string) - >> (Toplevel.theory oo fold) (fn (target, syns) => - fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns) - ); + process_multi_syntax Parse.xname (Scan.option Parse.string) + add_syntax_class_cmd); val _ = Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl ( - parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname) + process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname) (Scan.option (Parse.minus >> K ())) - >> (Toplevel.theory oo fold) (fn (target, syns) => - fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns) - ); + add_syntax_inst_cmd); val _ = Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl ( - parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I) - >> (Toplevel.theory oo fold) (fn (target, syns) => - fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns) - ); + process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax + add_syntax_tyco_cmd); val _ = Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl ( - parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst) - >> (Toplevel.theory oo fold) (fn (target, syns) => - fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns) - ); + process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax + add_syntax_const_cmd); val _ = Outer_Syntax.command "code_reserved" "declare words as reserved for target language"