1.1 --- a/src/Tools/Code/code_printer.ML	Sat May 18 13:04:10 2013 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Sun May 19 20:15:00 2013 +0200
     1.3 @@ -73,8 +73,8 @@
     1.4    datatype activated_const_syntax = Plain_const_syntax of int * string
     1.5      | Complex_const_syntax of activated_complex_const_syntax
     1.6    val requires_args: const_syntax -> int
     1.7 -  val parse_const_syntax: Token.T list -> const_syntax option * Token.T list
     1.8 -  val parse_tyco_syntax: Token.T list -> tyco_syntax option * Token.T list
     1.9 +  val parse_const_syntax: Token.T list -> const_syntax * Token.T list
    1.10 +  val parse_tyco_syntax: Token.T list -> tyco_syntax * Token.T list
    1.11    val plain_const_syntax: string -> const_syntax
    1.12    val simple_const_syntax: simple_const_syntax -> const_syntax
    1.13    val complex_const_syntax: complex_const_syntax -> const_syntax
    1.14 @@ -387,13 +387,12 @@
    1.15    end;
    1.16  
    1.17  fun parse_syntax mk_plain mk_complex prep_arg =
    1.18 -  Scan.option (
    1.19 -      ((@{keyword "infix"} >> K X)
    1.20 -        || (@{keyword "infixl"} >> K L)
    1.21 -        || (@{keyword "infixr"} >> K R))
    1.22 -        -- Parse.nat -- Parse.string
    1.23 -        >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
    1.24 -      || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
    1.25 +  ((@{keyword "infix"} >> K X)
    1.26 +    || (@{keyword "infixl"} >> K L)
    1.27 +    || (@{keyword "infixr"} >> K R))
    1.28 +    -- Parse.nat -- Parse.string
    1.29 +    >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
    1.30 +  || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s));
    1.31  
    1.32  fun parse_tyco_syntax x = parse_syntax (fn s => (0, (K o K o K o str) s)) I I x;
    1.33  

     2.1 --- a/src/Tools/Code/code_target.ML	Sat May 18 13:04:10 2013 +0200
     2.2 +++ b/src/Tools/Code/code_target.ML	Sun May 19 20:15:00 2013 +0200
     2.3 @@ -647,7 +647,7 @@
     2.4  fun process_multi_syntax parse_thing parse_syntax change =
     2.5    (Parse.and_list1 parse_thing
     2.6    :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
     2.7 -        (zip_list things parse_syntax @{keyword "and"}) --| @{keyword ")"})))
     2.8 +        (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"})))
     2.9    >> (Toplevel.theory oo fold)
    2.10      (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
    2.11  
    2.12 @@ -689,24 +689,21 @@
    2.13  
    2.14  val _ =
    2.15    Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
    2.16 -    (process_multi_syntax Parse.xname (Scan.option Parse.string)
    2.17 +    (process_multi_syntax Parse.xname Parse.string
    2.18        add_class_syntax_cmd);
    2.19  
    2.20  val _ =
    2.21    Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
    2.22 -    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
    2.23 -      (Scan.option (Parse.minus >> K ()))
    2.24 +    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) (Parse.minus >> K ())
    2.25        add_instance_syntax_cmd);
    2.26  
    2.27  val _ =
    2.28    Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
    2.29 -    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
    2.30 -      add_tyco_syntax_cmd);
    2.31 +    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax add_tyco_syntax_cmd);
    2.32  
    2.33  val _ =
    2.34    Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
    2.35 -    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
    2.36 -      add_const_syntax_cmd);
    2.37 +    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax add_const_syntax_cmd);
    2.38  
    2.39  val _ =
    2.40    Outer_Syntax.command @{command_spec "code_reserved"}