src/Pure/Tools/codegen_thingol.ML
changeset 18852 f1e2602ca7ba
parent 18850 92ef83e5eaea
child 18865 31aed965135c
equal deleted inserted replaced
18851:9502ce541f01 18852:f1e2602ca7ba
   505       ]
   505       ]
   506   | pretty_def (Datatype ((vs, cs), insts)) =
   506   | pretty_def (Datatype ((vs, cs), insts)) =
   507       Pretty.block [
   507       Pretty.block [
   508         Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
   508         Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
   509         Pretty.str " |=> ",
   509         Pretty.str " |=> ",
   510         Pretty.gen_list " |" "" ""
   510         Pretty.enum " |" "" ""
   511           (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
   511           (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
   512             (Pretty.str c :: map pretty_itype tys)) cs),
   512             (Pretty.str c :: map pretty_itype tys)) cs),
   513         Pretty.str ", instances ",
   513         Pretty.str ", instances ",
   514         Pretty.enum "," "[" "]" (map Pretty.str insts)
   514         Pretty.enum "," "[" "]" (map Pretty.str insts)
   515       ]
   515       ]
   518   | pretty_def (Class ((supcls, (v, mems)), insts)) =
   518   | pretty_def (Class ((supcls, (v, mems)), insts)) =
   519       Pretty.block [
   519       Pretty.block [
   520         Pretty.str ("class var " ^ v ^ "extending "),
   520         Pretty.str ("class var " ^ v ^ "extending "),
   521         Pretty.enum "," "[" "]" (map Pretty.str supcls),
   521         Pretty.enum "," "[" "]" (map Pretty.str supcls),
   522         Pretty.str " with ",
   522         Pretty.str " with ",
   523         Pretty.gen_list "," "[" "]"
   523         Pretty.enum "," "[" "]"
   524           (map (fn (m, (_, ty)) => Pretty.block
   524           (map (fn (m, (_, ty)) => Pretty.block
   525             [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
   525             [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
   526         Pretty.str " instances ",
   526         Pretty.str " instances ",
   527         Pretty.enum "," "[" "]" (map Pretty.str insts)
   527         Pretty.enum "," "[" "]" (map Pretty.str insts)
   528       ]
   528       ]
   536         Pretty.str "class instance (",
   536         Pretty.str "class instance (",
   537         Pretty.str clsname,
   537         Pretty.str clsname,
   538         Pretty.str ", (",
   538         Pretty.str ", (",
   539         Pretty.str tyco,
   539         Pretty.str tyco,
   540         Pretty.str ", ",
   540         Pretty.str ", ",
   541         Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o
   541         Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
   542           map Pretty.str o snd) arity),
   542           map Pretty.str o snd) arity),
   543         Pretty.str "))"
   543         Pretty.str "))"
   544       ];
   544       ];
   545 
   545 
   546 fun pretty_module modl =
   546 fun pretty_module modl =