src/Tools/Code/code_haskell.ML
changeset 36576 736994daaf08
parent 36535 0195ef994077
child 36960 01594f816e3a
equal deleted inserted replaced
36544:8da6846b87d9 36576:736994daaf08
   107           let
   107           let
   108             fun print_select (pat, body) =
   108             fun print_select (pat, body) =
   109               let
   109               let
   110                 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
   110                 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
   111               in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
   111               in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
   112           in brackify_block fxy
   112           in Pretty.block_enclose
   113             (concat [str "case", print_term tyvars some_thm vars NOBR t, str "of", str "{"])
   113             (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
   114             (map print_select clauses)
   114             (map print_select clauses)
   115             (str "}") 
       
   116           end
   115           end
   117       | print_case tyvars some_thm vars fxy ((_, []), _) =
   116       | print_case tyvars some_thm vars fxy ((_, []), _) =
   118           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
   117           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
   119     fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
   118     fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
   120           let
   119           let