src/Tools/code/code_ml.ML
changeset 31665 a1f4d3b3f6c8
parent 31598 946a7a175bf1
child 31724 9b5a128cdb5c
equal deleted inserted replaced
31643:b040f1679f77 31665:a1f4d3b3f6c8
   149                 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
   149                 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
   150               in
   150               in
   151                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
   151                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
   152               end;
   152               end;
   153           in
   153           in
   154             (Pretty.enclose "(" ")" o single o brackify fxy) (
   154             brackets (
   155               str "case"
   155               str "case"
   156               :: pr_term is_closure thm vars NOBR t
   156               :: pr_term is_closure thm vars NOBR t
   157               :: pr "of" clause
   157               :: pr "of" clause
   158               :: map (pr "|") clauses
   158               :: map (pr "|") clauses
   159             )
   159             )
   439               vars
   439               vars
   440               |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
   440               |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
   441               |>> (fn p => concat
   441               |>> (fn p => concat
   442                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
   442                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
   443             val (ps, vars') = fold_map pr binds vars;
   443             val (ps, vars') = fold_map pr binds vars;
   444             fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
   444           in
   445           in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
   445             brackify_block fxy (Pretty.chunks ps) []
       
   446               (pr_term is_closure thm vars' NOBR body)
       
   447           end
   446       | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
   448       | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
   447           let
   449           let
   448             fun pr delim (pat, body) =
   450             fun pr delim (pat, body) =
   449               let
   451               let
   450                 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
   452                 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
   451               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
   453               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
   452           in
   454           in
   453             (Pretty.enclose "(" ")" o single o brackify fxy) (
   455             brackets (
   454               str "match"
   456               str "match"
   455               :: pr_term is_closure thm vars NOBR t
   457               :: pr_term is_closure thm vars NOBR t
   456               :: pr "with" clause
   458               :: pr "with" clause
   457               :: map (pr "|") clauses
   459               :: map (pr "|") clauses
   458             )
   460             )