src/Pure/Tools/codegen_serializer.ML
changeset 20439 1bf42b262a38
parent 20428 67fa1c6ba89e
child 20456 42be3a46dcd8
     1.1 --- a/src/Pure/Tools/codegen_serializer.ML	Wed Aug 30 12:28:39 2006 +0200
     1.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Wed Aug 30 15:11:17 2006 +0200
     1.3 @@ -166,36 +166,34 @@
     1.4      | _ => error ("Malformed mixfix annotation: " ^ quote s)
     1.5    end;
     1.6  
     1.7 -fun parse_nonatomic_mixfix reader s ctxt =
     1.8 -  case parse_mixfix reader s ctxt
     1.9 -   of ([Pretty _], _) =>
    1.10 -        error ("Mixfix contains just one pretty element; either declare as "
    1.11 -          ^ quote atomK ^ " or consider adding a break")
    1.12 -    | x => x;
    1.13 -
    1.14 -fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- (
    1.15 -       OuterParse.$$$ infixK  |-- OuterParse.nat
    1.16 -        >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
    1.17 -    || OuterParse.$$$ infixlK |-- OuterParse.nat
    1.18 -        >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
    1.19 -    || OuterParse.$$$ infixrK |-- OuterParse.nat
    1.20 -        >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
    1.21 -    || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
    1.22 -    || pair (parse_nonatomic_mixfix reader, BR)
    1.23 -  ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
    1.24 -
    1.25 -fun parse_syntax no_args reader =
    1.26 +fun parse_syntax num_args reader =
    1.27    let
    1.28      fun is_arg (Arg _) = true
    1.29        | is_arg Ignore = true
    1.30        | is_arg _ = false;
    1.31 +    fun parse_nonatomic s ctxt =
    1.32 +      case parse_mixfix reader s ctxt
    1.33 +       of ([Pretty _], _) =>
    1.34 +            error ("Mixfix contains just one pretty element; either declare as "
    1.35 +              ^ quote atomK ^ " or consider adding a break")
    1.36 +        | x => x;
    1.37 +    val parse = OuterParse.$$$ "(" |-- (
    1.38 +           OuterParse.$$$ infixK  |-- OuterParse.nat
    1.39 +            >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
    1.40 +        || OuterParse.$$$ infixlK |-- OuterParse.nat
    1.41 +            >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
    1.42 +        || OuterParse.$$$ infixrK |-- OuterParse.nat
    1.43 +            >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
    1.44 +        || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
    1.45 +        || pair (parse_nonatomic, BR)
    1.46 +      ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
    1.47      fun mk fixity mfx ctxt =
    1.48        let
    1.49          val i = (length o List.filter is_arg) mfx;
    1.50 -        val _ = if i > no_args ctxt then error "Too many arguments in codegen syntax" else ();
    1.51 +        val _ = if i > num_args ctxt then error "Too many arguments in codegen syntax" else ();
    1.52        in (((i, i), fillin_mixfix fixity mfx), ctxt) end;
    1.53    in
    1.54 -    parse_syntax_proto reader
    1.55 +    parse
    1.56      #-> (fn (mfx_reader, fixity) =>
    1.57        pair (mfx_reader #-> (fn mfx => mk fixity mfx))
    1.58      )