src/Tools/Code/code_target.ML
changeset 52068 1abaea5d5a22
parent 51685 385ef6706252
child 52137 7f7337447b1b
     1.1 --- a/src/Tools/Code/code_target.ML	Sat May 18 13:04:10 2013 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Sun May 19 20:15:00 2013 +0200
     1.3 @@ -647,7 +647,7 @@
     1.4  fun process_multi_syntax parse_thing parse_syntax change =
     1.5    (Parse.and_list1 parse_thing
     1.6    :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
     1.7 -        (zip_list things parse_syntax @{keyword "and"}) --| @{keyword ")"})))
     1.8 +        (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"})))
     1.9    >> (Toplevel.theory oo fold)
    1.10      (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
    1.11  
    1.12 @@ -689,24 +689,21 @@
    1.13  
    1.14  val _ =
    1.15    Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
    1.16 -    (process_multi_syntax Parse.xname (Scan.option Parse.string)
    1.17 +    (process_multi_syntax Parse.xname Parse.string
    1.18        add_class_syntax_cmd);
    1.19  
    1.20  val _ =
    1.21    Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
    1.22 -    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
    1.23 -      (Scan.option (Parse.minus >> K ()))
    1.24 +    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) (Parse.minus >> K ())
    1.25        add_instance_syntax_cmd);
    1.26  
    1.27  val _ =
    1.28    Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
    1.29 -    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
    1.30 -      add_tyco_syntax_cmd);
    1.31 +    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax add_tyco_syntax_cmd);
    1.32  
    1.33  val _ =
    1.34    Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
    1.35 -    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
    1.36 -      add_const_syntax_cmd);
    1.37 +    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax add_const_syntax_cmd);
    1.38  
    1.39  val _ =
    1.40    Outer_Syntax.command @{command_spec "code_reserved"}