# HG changeset patch # User haftmann # Date 1368987300 -7200 # Node ID 1abaea5d5a22bfdd746503946661c0a3b1904022 # Parent 4894df243482a4b81af3f3f07291dfe0631aa8c9 tuned, including signature diff -r 4894df243482 -r 1abaea5d5a22 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Sat May 18 13:04:10 2013 +0200 +++ b/src/Tools/Code/code_printer.ML Sun May 19 20:15:00 2013 +0200 @@ -73,8 +73,8 @@ 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 parse_const_syntax: Token.T list -> const_syntax * Token.T list + val parse_tyco_syntax: Token.T list -> tyco_syntax * 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 @@ -387,13 +387,12 @@ end; fun parse_syntax mk_plain mk_complex prep_arg = - Scan.option ( - ((@{keyword "infix"} >> K X) - || (@{keyword "infixl"} >> K L) - || (@{keyword "infixr"} >> K R)) - -- 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))); + ((@{keyword "infix"} >> K X) + || (@{keyword "infixl"} >> K L) + || (@{keyword "infixr"} >> K R)) + -- 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)); fun parse_tyco_syntax x = parse_syntax (fn s => (0, (K o K o K o str) s)) I I x; diff -r 4894df243482 -r 1abaea5d5a22 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sat May 18 13:04:10 2013 +0200 +++ b/src/Tools/Code/code_target.ML Sun May 19 20:15:00 2013 +0200 @@ -647,7 +647,7 @@ fun process_multi_syntax parse_thing parse_syntax change = (Parse.and_list1 parse_thing :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name -- - (zip_list things parse_syntax @{keyword "and"}) --| @{keyword ")"}))) + (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"}))) >> (Toplevel.theory oo fold) (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns); @@ -689,24 +689,21 @@ val _ = Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class" - (process_multi_syntax Parse.xname (Scan.option Parse.string) + (process_multi_syntax Parse.xname Parse.string add_class_syntax_cmd); val _ = Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance" - (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) - (Scan.option (Parse.minus >> K ())) + (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) (Parse.minus >> K ()) add_instance_syntax_cmd); val _ = Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor" - (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax - add_tyco_syntax_cmd); + (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax add_tyco_syntax_cmd); val _ = Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant" - (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax - add_const_syntax_cmd); + (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax add_const_syntax_cmd); val _ = Outer_Syntax.command @{command_spec "code_reserved"}