# HG changeset patch # User berghofe # Date 1211553699 -7200 # Node ID 103dca19ef2ee8aa2fa8106ca0d84c67e06e8efe # Parent 83adc1eaeaabd586495818fda29f029fd880ce2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately. diff -r 83adc1eaeaab -r 103dca19ef2e src/HOL/Code_Setup.thy --- a/src/HOL/Code_Setup.thy Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/Code_Setup.thy Fri May 23 16:41:39 2008 +0200 @@ -52,7 +52,7 @@ val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) in SOME (gr''', Codegen.parens - (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) + (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu])) end | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) diff -r 83adc1eaeaab -r 103dca19ef2e src/HOL/Int.thy --- a/src/HOL/Int.thy Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/Int.thy Fri May 23 16:41:39 2008 +0200 @@ -1979,7 +1979,7 @@ let val i = HOLogic.dest_numeral (strip_number_of t) in SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)), - Pretty.str (string_of_int i)) + Codegen.str (string_of_int i)) end handle TERM _ => NONE; in diff -r 83adc1eaeaab -r 103dca19ef2e src/HOL/List.thy --- a/src/HOL/List.thy Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/List.thy Fri May 23 16:41:39 2008 +0200 @@ -3410,7 +3410,7 @@ val i = HOLogic.dest_char t; val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr, fastype_of t) - in SOME (gr', Pretty.str (ML_Syntax.print_string (chr i))) + in SOME (gr', Codegen.str (ML_Syntax.print_string (chr i))) end handle TERM _ => NONE; in diff -r 83adc1eaeaab -r 103dca19ef2e src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/Product_Type.thy Fri May 23 16:41:39 2008 +0200 @@ -1008,12 +1008,12 @@ (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts) in SOME (gr3, Codegen.mk_app brack - (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat - (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) => - [Pretty.block [Pretty.str "val ", pl, Pretty.str " =", + (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat + (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) => + [Pretty.block [Codegen.str "val ", pl, Codegen.str " =", Pretty.brk 1, pr]]) qs))), - Pretty.brk 1, Pretty.str "in ", pu, - Pretty.brk 1, Pretty.str "end"])) pargs) + Pretty.brk 1, Codegen.str "in ", pu, + Pretty.brk 1, Codegen.str "end"])) pargs) end end | _ => NONE); @@ -1029,8 +1029,8 @@ (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts) in SOME (gr2, Codegen.mk_app brack - (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>", - Pretty.brk 1, pu, Pretty.str ")"]) pargs) + (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>", + Pretty.brk 1, pu, Codegen.str ")"]) pargs) end | _ => NONE) | _ => NONE); diff -r 83adc1eaeaab -r 103dca19ef2e src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Fri May 23 16:41:39 2008 +0200 @@ -62,23 +62,23 @@ val (gr''', rest) = mk_dtdef gr'' "and " xs in (gr''', - Pretty.block (Pretty.str prfx :: + Pretty.block (str prfx :: (if null tvs then [] else - [mk_tuple (map Pretty.str tvs), Pretty.str " "]) @ - [Pretty.str (type_id ^ " ="), Pretty.brk 1] @ - List.concat (separate [Pretty.brk 1, Pretty.str "| "] + [mk_tuple (map str tvs), str " "]) @ + [str (type_id ^ " ="), Pretty.brk 1] @ + List.concat (separate [Pretty.brk 1, str "| "] (map (fn (ps', (_, cname)) => [Pretty.block - (Pretty.str cname :: + (str cname :: (if null ps' then [] else - List.concat ([Pretty.str " of", Pretty.brk 1] :: - separate [Pretty.str " *", Pretty.brk 1] + List.concat ([str " of", Pretty.brk 1] :: + separate [str " *", Pretty.brk 1] (map single ps'))))]) ps))) :: rest) end; fun mk_constr_term cname Ts T ps = - List.concat (separate [Pretty.str " $", Pretty.brk 1] - ([Pretty.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1, - mk_type false (Ts ---> T), Pretty.str ")"] :: ps)); + List.concat (separate [str " $", Pretty.brk 1] + ([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1, + mk_type false (Ts ---> T), str ")"] :: ps)); fun mk_term_of_def gr prfx [] = [] | mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) = @@ -89,14 +89,14 @@ val rest = mk_term_of_def gr "and " xs; val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) => let val args = map (fn i => - Pretty.str ("x" ^ string_of_int i)) (1 upto length Ts) + str ("x" ^ string_of_int i)) (1 upto length Ts) in (" | ", Pretty.blk (4, - [Pretty.str prfx, mk_term_of gr module' false T, Pretty.brk 1, - if null Ts then Pretty.str (snd (get_const_id cname gr)) + [str prfx, mk_term_of gr module' false T, Pretty.brk 1, + if null Ts then str (snd (get_const_id cname gr)) else parens (Pretty.block - [Pretty.str (snd (get_const_id cname gr)), + [str (snd (get_const_id cname gr)), Pretty.brk 1, mk_tuple args]), - Pretty.str " =", Pretty.brk 1] @ + str " =", Pretty.brk 1] @ mk_constr_term cname Ts T (map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U, Pretty.brk 1, x]]) (args ~~ Ts)))) @@ -114,20 +114,20 @@ val SOME (cname, _) = find_nonempty descr [i] i; fun mk_delay p = Pretty.block - [Pretty.str "fn () =>", Pretty.brk 1, p]; + [str "fn () =>", Pretty.brk 1, p]; - fun mk_force p = Pretty.block [p, Pretty.brk 1, Pretty.str "()"]; + fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"]; fun mk_constr s b (cname, dts) = let val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s (DatatypeAux.typ_of_dtyp descr sorts dt)) - [Pretty.str (if b andalso DatatypeAux.is_rec_type dt then "0" + [str (if b andalso DatatypeAux.is_rec_type dt then "0" else "j")]) dts; val Ts = map (DatatypeAux.typ_of_dtyp descr sorts) dts; - val xs = map Pretty.str + val xs = map str (DatatypeProp.indexify_names (replicate (length dts) "x")); - val ts = map Pretty.str + val ts = map str (DatatypeProp.indexify_names (replicate (length dts) "t")); val (_, id) = get_const_id cname gr in @@ -136,52 +136,52 @@ (mk_tuple [case xs of _ :: _ :: _ => Pretty.block - [Pretty.str id, Pretty.brk 1, mk_tuple xs] - | _ => mk_app false (Pretty.str id) xs, + [str id, Pretty.brk 1, mk_tuple xs] + | _ => mk_app false (str id) xs, mk_delay (Pretty.block (mk_constr_term cname Ts T (map (single o mk_force) ts)))]) end; fun mk_choice [c] = mk_constr "(i-1)" false c - | mk_choice cs = Pretty.block [Pretty.str "one_of", - Pretty.brk 1, Pretty.blk (1, Pretty.str "[" :: - List.concat (separate [Pretty.str ",", Pretty.fbrk] + | mk_choice cs = Pretty.block [str "one_of", + Pretty.brk 1, Pretty.blk (1, str "[" :: + List.concat (separate [str ",", Pretty.fbrk] (map (single o mk_delay o mk_constr "(i-1)" false) cs)) @ - [Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"]; + [str "]"]), Pretty.brk 1, str "()"]; val gs = maps (fn s => let val s' = strip_tname s - in [Pretty.str (s' ^ "G"), Pretty.str (s' ^ "T")] end) tvs; + in [str (s' ^ "G"), str (s' ^ "T")] end) tvs; val gen_name = "gen_" ^ snd (get_type_id tname gr) in Pretty.blk (4, separate (Pretty.brk 1) - (Pretty.str (prfx ^ gen_name ^ + (str (prfx ^ gen_name ^ (if null cs1 then "" else "'")) :: gs @ - (if null cs1 then [] else [Pretty.str "i"]) @ - [Pretty.str "j"]) @ - [Pretty.str " =", Pretty.brk 1] @ + (if null cs1 then [] else [str "i"]) @ + [str "j"]) @ + [str " =", Pretty.brk 1] @ (if not (null cs1) andalso not (null cs2) - then [Pretty.str "frequency", Pretty.brk 1, - Pretty.blk (1, [Pretty.str "[", - mk_tuple [Pretty.str "i", mk_delay (mk_choice cs1)], - Pretty.str ",", Pretty.fbrk, - mk_tuple [Pretty.str "1", mk_delay (mk_choice cs2)], - Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"] + then [str "frequency", Pretty.brk 1, + Pretty.blk (1, [str "[", + mk_tuple [str "i", mk_delay (mk_choice cs1)], + str ",", Pretty.fbrk, + mk_tuple [str "1", mk_delay (mk_choice cs2)], + str "]"]), Pretty.brk 1, str "()"] else if null cs2 then - [Pretty.block [Pretty.str "(case", Pretty.brk 1, - Pretty.str "i", Pretty.brk 1, Pretty.str "of", - Pretty.brk 1, Pretty.str "0 =>", Pretty.brk 1, + [Pretty.block [str "(case", Pretty.brk 1, + str "i", Pretty.brk 1, str "of", + Pretty.brk 1, str "0 =>", Pretty.brk 1, mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)), - Pretty.brk 1, Pretty.str "| _ =>", Pretty.brk 1, - mk_choice cs1, Pretty.str ")"]] + Pretty.brk 1, str "| _ =>", Pretty.brk 1, + mk_choice cs1, str ")"]] else [mk_choice cs2])) :: (if null cs1 then [] else [Pretty.blk (4, separate (Pretty.brk 1) - (Pretty.str ("and " ^ gen_name) :: gs @ [Pretty.str "i"]) @ - [Pretty.str " =", Pretty.brk 1] @ - separate (Pretty.brk 1) (Pretty.str (gen_name ^ "'") :: gs @ - [Pretty.str "i", Pretty.str "i"]))]) @ + (str ("and " ^ gen_name) :: gs @ [str "i"]) @ + [str " =", Pretty.brk 1] @ + separate (Pretty.brk 1) (str (gen_name ^ "'") :: gs @ + [str "i", str "i"]))]) @ mk_gen_of_def gr "and " xs end @@ -194,15 +194,15 @@ val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr'; in map_node node_id (K (NONE, module', - Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ - [Pretty.str ";"])) ^ "\n\n" ^ + string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ + [str ";"])) ^ "\n\n" ^ (if "term_of" mem !mode then - Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk - (mk_term_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" + string_of (Pretty.blk (0, separate Pretty.fbrk + (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n" else "") ^ (if "test" mem !mode then - Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk - (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" + string_of (Pretty.blk (0, separate Pretty.fbrk + (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n" else ""))) gr2 end, module') @@ -236,17 +236,17 @@ val (gr1, p) = invoke_codegen thy defs dep module false (gr0, t'); val (ps, gr2) = pcase gr1 cs ts Us; in - ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2) + ([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2) end; val (ps1, gr1) = pcase gr constrs ts1 Ts; - val ps = List.concat (separate [Pretty.brk 1, Pretty.str "| "] ps1); + val ps = List.concat (separate [Pretty.brk 1, str "| "] ps1); val (gr2, p) = invoke_codegen thy defs dep module false (gr1, t); val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep module true) (gr2, ts2) in (gr3, (if not (null ts2) andalso brack then parens else I) (Pretty.block (separate (Pretty.brk 1) - (Pretty.block ([Pretty.str "(case ", p, Pretty.str " of", - Pretty.brk 1] @ ps @ [Pretty.str ")"]) :: ps2)))) + (Pretty.block ([str "(case ", p, str " of", + Pretty.brk 1] @ ps @ [str ")"]) :: ps2)))) end end; @@ -264,8 +264,8 @@ (invoke_codegen thy defs dep module (i = 1)) (gr, ts); in (case args of _ :: _ :: _ => (gr', (if brack then parens else I) - (Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps])) - | _ => (gr', mk_app brack (Pretty.str id) ps)) + (Pretty.block [str id, Pretty.brk 1, mk_tuple ps])) + | _ => (gr', mk_app brack (str id) ps)) end end; @@ -304,8 +304,8 @@ val (gr''', tyid) = mk_type_id module' s gr'' in SOME (gr''', Pretty.block ((if null Ts then [] else - [mk_tuple ps, Pretty.str " "]) @ - [Pretty.str (mk_qual_id module tyid)])) + [mk_tuple ps, str " "]) @ + [str (mk_qual_id module tyid)])) end) | datatype_tycodegen _ _ _ _ _ _ _ = NONE; diff -r 83adc1eaeaab -r 103dca19ef2e src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Fri May 23 16:41:39 2008 +0200 @@ -260,12 +260,12 @@ fun mk_eq (x::xs) = let fun mk_eqs _ [] = [] - | mk_eqs a (b::cs) = Pretty.str (a ^ " = " ^ b) :: mk_eqs b cs + | mk_eqs a (b::cs) = str (a ^ " = " ^ b) :: mk_eqs b cs in mk_eqs x xs end; -fun mk_tuple xs = Pretty.block (Pretty.str "(" :: - List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @ - [Pretty.str ")"]); +fun mk_tuple xs = Pretty.block (str "(" :: + List.concat (separate [str ",", Pretty.brk 1] (map single xs)) @ + [str ")"]); fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of NONE => ((names, (s, [s])::vs), s) @@ -287,18 +287,18 @@ | is_exhaustive _ = false; fun compile_match nvs eq_ps out_ps success_p can_fail = - let val eqs = List.concat (separate [Pretty.str " andalso", Pretty.brk 1] + let val eqs = List.concat (separate [str " andalso", Pretty.brk 1] (map single (List.concat (map (mk_eq o snd) nvs) @ eq_ps))); in Pretty.block - ([Pretty.str "(fn ", mk_tuple out_ps, Pretty.str " =>", Pretty.brk 1] @ - (Pretty.block ((if eqs=[] then [] else Pretty.str "if " :: - [Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @ + ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @ + (Pretty.block ((if eqs=[] then [] else str "if " :: + [Pretty.block eqs, Pretty.brk 1, str "then "]) @ (success_p :: - (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else DSeq.empty"]))) :: + (if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) :: (if can_fail then - [Pretty.brk 1, Pretty.str "| _ => DSeq.empty)"] - else [Pretty.str ")"]))) + [Pretty.brk 1, str "| _ => DSeq.empty)"] + else [str ")"]))) end; fun modename module s (iss, is) gr = @@ -310,14 +310,14 @@ end; fun mk_funcomp brack s k p = (if brack then parens else I) - (Pretty.block [Pretty.block ((if k = 0 then [] else [Pretty.str "("]) @ - separate (Pretty.brk 1) (Pretty.str s :: replicate k (Pretty.str "|> ???")) @ - (if k = 0 then [] else [Pretty.str ")"])), Pretty.brk 1, p]); + (Pretty.block [Pretty.block ((if k = 0 then [] else [str "("]) @ + separate (Pretty.brk 1) (str s :: replicate k (str "|> ???")) @ + (if k = 0 then [] else [str ")"])), Pretty.brk 1, p]); fun compile_expr thy defs dep module brack modes (gr, (NONE, t)) = apsnd single (invoke_codegen thy defs dep module brack (gr, t)) | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) = - (gr, [Pretty.str name]) + (gr, [str name]) | compile_expr thy defs dep module brack modes (gr, (SOME (Mode (mode, _, ms)), t)) = (case strip_comb t of (Const (name, _), args) => @@ -328,13 +328,13 @@ (compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>> modename module name mode; val (gr'', ps') = (case mode of - ([], []) => (gr', [Pretty.str "()"]) + ([], []) => (gr', [str "()"]) | _ => foldl_map (invoke_codegen thy defs dep module true) (gr', args2)) in (gr', (if brack andalso not (null ps andalso null ps') then single o parens o Pretty.block else I) (List.concat (separate [Pretty.brk 1] - ([Pretty.str mode_id] :: ps @ map single ps')))) + ([str mode_id] :: ps @ map single ps')))) end else apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) (invoke_codegen thy defs dep module true (gr, t)) @@ -353,7 +353,7 @@ in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end; fun compile_eq (gr, (s, t)) = - apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single) + apsnd (Pretty.block o cons (str (s ^ " = ")) o single) (invoke_codegen thy defs dep module false (gr, t)); val (in_ts, out_ts) = get_args is 1 ts; @@ -374,7 +374,7 @@ val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs') in (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps' - (Pretty.block [Pretty.str "DSeq.single", Pretty.brk 1, mk_tuple out_ps]) + (Pretty.block [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps]) (exists (not o is_exhaustive) out_ts''')) end | compile_prems out_ts vs names gr ps = @@ -405,13 +405,13 @@ (compile_expr thy defs dep module false modes (gr2, (mode, t))) else - apsnd (fn p => [Pretty.str "DSeq.of_list", Pretty.brk 1, p]) + apsnd (fn p => [str "DSeq.of_list", Pretty.brk 1, p]) (invoke_codegen thy defs dep module true (gr2, t)); val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps'; in (gr4, compile_match (snd nvs) eq_ps out_ps (Pretty.block (ps @ - [Pretty.str " :->", Pretty.brk 1, rest])) + [str " :->", Pretty.brk 1, rest])) (exists (not o is_exhaustive) out_ts'')) end | Sidecond t => @@ -420,21 +420,21 @@ val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps'; in (gr3, compile_match (snd nvs) eq_ps out_ps - (Pretty.block [Pretty.str "?? ", side_p, - Pretty.str " :->", Pretty.brk 1, rest]) + (Pretty.block [str "?? ", side_p, + str " :->", Pretty.brk 1, rest]) (exists (not o is_exhaustive) out_ts'')) end) end; val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps; in - (gr', Pretty.block [Pretty.str "DSeq.single", Pretty.brk 1, inp, - Pretty.str " :->", Pretty.brk 1, prem_p]) + (gr', Pretty.block [str "DSeq.single", Pretty.brk 1, inp, + str " :->", Pretty.brk 1, prem_p]) end; fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode = let - val xs = map Pretty.str (Name.variant_list arg_vs + val xs = map str (Name.variant_list arg_vs (map (fn i => "x" ^ string_of_int i) (snd mode))); val (gr', (cl_ps, mode_id)) = foldl_map (fn (gr, cl) => compile_clause thy defs @@ -443,12 +443,12 @@ in ((gr', "and "), Pretty.block ([Pretty.block (separate (Pretty.brk 1) - (Pretty.str (prfx ^ mode_id) :: - map Pretty.str arg_vs @ - (case mode of ([], []) => [Pretty.str "()"] | _ => xs)) @ - [Pretty.str " ="]), + (str (prfx ^ mode_id) :: + map str arg_vs @ + (case mode of ([], []) => [str "()"] | _ => xs)) @ + [str " ="]), Pretty.brk 1] @ - List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps)))) + List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps)))) end; fun compile_preds thy defs gr dep module all_vs arg_vs modes preds = @@ -457,7 +457,7 @@ dep module prfx' all_vs arg_vs modes s cls mode) ((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds) in - (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n") + (gr', space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n") end; (**** processing of introduction rules ****) @@ -605,11 +605,11 @@ val (gr', (fun_id, mode_id)) = gr |> mk_const_id module' name |>>> modename module' pname ([], mode); - val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode; - val s = Pretty.string_of (Pretty.block - [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =", - Pretty.brk 1, Pretty.str "DSeq.hd", Pretty.brk 1, - parens (Pretty.block (separate (Pretty.brk 1) (Pretty.str mode_id :: + val vars = map (fn i => str ("x" ^ string_of_int i)) mode; + val s = string_of (Pretty.block + [mk_app false (str ("fun " ^ snd fun_id)) vars, str " =", + Pretty.brk 1, str "DSeq.hd", Pretty.brk 1, + parens (Pretty.block (separate (Pretty.brk 1) (str mode_id :: vars)))]) ^ ";\n\n"; val gr'' = mk_ind_def thy defs (add_edge (name, dep) (new_node (name, (NONE, module', s)) gr')) name [pname] module' @@ -626,7 +626,7 @@ fun conv_ntuple fs ts p = let val k = length fs; - val xs = map (fn i => Pretty.str ("x" ^ string_of_int i)) (0 upto k); + val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k); val xs' = map (fn Bound i => nth xs (k - i)) ts; fun conv xs js = if js mem fs then @@ -638,9 +638,9 @@ in if k > 0 then Pretty.block - [Pretty.str "DSeq.map (fn", Pretty.brk 1, - mk_tuple xs', Pretty.str " =>", Pretty.brk 1, fst (conv xs []), - Pretty.str ")", Pretty.brk 1, parens p] + [str "DSeq.map (fn", Pretty.brk 1, + mk_tuple xs', str " =>", Pretty.brk 1, fst (conv xs []), + str ")", Pretty.brk 1, parens p] else p end; @@ -664,8 +664,8 @@ let val (gr', call_p) = mk_ind_call thy defs gr dep module true s T (ts1 @ ts2') names thyname k intrs in SOME (gr', (if brack then parens else I) (Pretty.block - [Pretty.str "DSeq.list_of", Pretty.brk 1, Pretty.str "(", - conv_ntuple fs ots call_p, Pretty.str ")"])) + [str "DSeq.list_of", Pretty.brk 1, str "(", + conv_ntuple fs ots call_p, str ")"])) end else NONE end @@ -690,7 +690,7 @@ dep module (if_library thyname module) gr; val (gr'', ps) = foldl_map (invoke_codegen thy defs dep module true) (gr', ts); - in SOME (gr'', mk_app brack (Pretty.str id) ps) + in SOME (gr'', mk_app brack (str id) ps) end) | _ => NONE); diff -r 83adc1eaeaab -r 103dca19ef2e src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Fri May 23 16:41:39 2008 +0200 @@ -105,13 +105,13 @@ val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs); val (gr3, rest) = mk_fundef module fname' false gr2 xs in - (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then " | " else prfx), - pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest) + (gr3, Pretty.blk (4, [str (if fname = fname' then " | " else prfx), + pl, str " =", Pretty.brk 1, pr]) :: rest) end; fun put_code module fundef = map_node dname - (K (SOME (EQN ("", dummyT, dname)), module, Pretty.string_of (Pretty.blk (0, - separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n")); + (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0, + separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n")); in (case try (get_node gr) dname of @@ -162,7 +162,7 @@ add_rec_funs thy defs gr' dep (map prop_of eqns) module'; val (gr''', fname) = mk_const_id module'' (s ^ suffix) gr'' in - SOME (gr''', mk_app brack (Pretty.str (mk_qual_id module fname)) ps) + SOME (gr''', mk_app brack (str (mk_qual_id module fname)) ps) end) | _ => NONE); diff -r 83adc1eaeaab -r 103dca19ef2e src/HOL/Tools/typedef_codegen.ML --- a/src/HOL/Tools/typedef_codegen.ML Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/Tools/typedef_codegen.ML Fri May 23 16:41:39 2008 +0200 @@ -23,7 +23,7 @@ val (gr'', ps) = foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts); val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'') - in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; + in SOME (gr'', Codegen.mk_app brack (Codegen.str id) ps) end; fun lookup f T = (case TypedefPackage.get_info thy (get_name T) of NONE => "" @@ -41,8 +41,8 @@ | _ => NONE) end; -fun mk_tyexpr [] s = Pretty.str s - | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)] +fun mk_tyexpr [] s = Codegen.str s + | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)] | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) = @@ -69,31 +69,31 @@ (Codegen.add_edge (node_id, dep) (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us); val s = - Pretty.string_of (Pretty.block [Pretty.str "datatype ", + Codegen.string_of (Pretty.block [Codegen.str "datatype ", mk_tyexpr ps (snd ty_id), - Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"), - Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^ - Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id), - Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1, - Pretty.str "x) = x;"]) ^ "\n\n" ^ + Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"), + Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^ + Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id), + Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, + Codegen.str "x) = x;"]) ^ "\n\n" ^ (if "term_of" mem !Codegen.mode then - Pretty.string_of (Pretty.block [Pretty.str "fun ", + Codegen.string_of (Pretty.block [Codegen.str "fun ", Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1, - Pretty.str ("(" ^ Abs_id), Pretty.brk 1, - Pretty.str "x) =", Pretty.brk 1, - Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","), + Codegen.str ("(" ^ Abs_id), Pretty.brk 1, + Codegen.str "x) =", Pretty.brk 1, + Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","), Pretty.brk 1, Codegen.mk_type false (oldT --> newT), - Pretty.str ")"], Pretty.str " $", Pretty.brk 1, + Codegen.str ")"], Codegen.str " $", Pretty.brk 1, Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1, - Pretty.str "x;"]) ^ "\n\n" + Codegen.str "x;"]) ^ "\n\n" else "") ^ (if "test" mem !Codegen.mode then - Pretty.string_of (Pretty.block [Pretty.str "fun ", + Codegen.string_of (Pretty.block [Codegen.str "fun ", Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1, - Pretty.str "i =", Pretty.brk 1, - Pretty.block [Pretty.str (Abs_id ^ " ("), + Codegen.str "i =", Pretty.brk 1, + Pretty.block [Codegen.str (Abs_id ^ " ("), Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1, - Pretty.str "i);"]]) ^ "\n\n" + Codegen.str "i);"]]) ^ "\n\n" else "") in Codegen.map_node node_id (K (NONE, module', s)) gr'' end | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)