src/Tools/Code/code_haskell.ML
changeset 58454 271829a473ed
parent 58400 d0d3c30806b4
child 59104 a14475f044b2
equal deleted inserted replaced
58453:75b92e25f59f 58454:271829a473ed
   469      of SOME (bind, t') => let
   469      of SOME (bind, t') => let
   470           val (binds, t'') = implode_monad t'
   470           val (binds, t'') = implode_monad t'
   471           val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
   471           val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
   472             (bind :: binds) vars;
   472             (bind :: binds) vars;
   473         in
   473         in
   474           (brackify fxy o single o enclose "do { " " }" o Pretty.breaks)
   474           brackify_block fxy (str "do { ")
   475             (ps @| print_term vars' NOBR t'')
   475             (ps @| print_term vars' NOBR t'')
       
   476             (str " }")
   476         end
   477         end
   477       | NONE => brackify_infix (1, L) fxy
   478       | NONE => brackify_infix (1, L) fxy
   478           (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
   479           (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
   479   in (2, pretty) end;
   480   in (2, pretty) end;
   480 
   481