Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
authorberghofe
Fri May 23 16:41:39 2008 +0200 (2008-05-23)
changeset 26975103dca19ef2e
parent 26974 83adc1eaeaab
child 26976 cf147f69b3df
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
set print_mode and margin appropriately.
src/HOL/Code_Setup.thy
src/HOL/Int.thy
src/HOL/List.thy
src/HOL/Product_Type.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/typedef_codegen.ML
     1.1 --- a/src/HOL/Code_Setup.thy	Fri May 23 16:37:57 2008 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Fri May 23 16:41:39 2008 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4              val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
     1.5            in
     1.6              SOME (gr''', Codegen.parens
     1.7 -              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
     1.8 +              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]))
     1.9            end
    1.10       | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.11           thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
     2.1 --- a/src/HOL/Int.thy	Fri May 23 16:37:57 2008 +0200
     2.2 +++ b/src/HOL/Int.thy	Fri May 23 16:41:39 2008 +0200
     2.3 @@ -1979,7 +1979,7 @@
     2.4    let val i = HOLogic.dest_numeral (strip_number_of t)
     2.5    in
     2.6      SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
     2.7 -      Pretty.str (string_of_int i))
     2.8 +      Codegen.str (string_of_int i))
     2.9    end handle TERM _ => NONE;
    2.10  
    2.11  in
     3.1 --- a/src/HOL/List.thy	Fri May 23 16:37:57 2008 +0200
     3.2 +++ b/src/HOL/List.thy	Fri May 23 16:41:39 2008 +0200
     3.3 @@ -3410,7 +3410,7 @@
     3.4      val i = HOLogic.dest_char t;
     3.5      val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
     3.6        (gr, fastype_of t)
     3.7 -  in SOME (gr', Pretty.str (ML_Syntax.print_string (chr i)))
     3.8 +  in SOME (gr', Codegen.str (ML_Syntax.print_string (chr i)))
     3.9    end handle TERM _ => NONE;
    3.10  
    3.11  in
     4.1 --- a/src/HOL/Product_Type.thy	Fri May 23 16:37:57 2008 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Fri May 23 16:41:39 2008 +0200
     4.3 @@ -1008,12 +1008,12 @@
     4.4                (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
     4.5            in
     4.6              SOME (gr3, Codegen.mk_app brack
     4.7 -              (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
     4.8 -                  (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
     4.9 -                    [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
    4.10 +              (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat
    4.11 +                  (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
    4.12 +                    [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
    4.13                         Pretty.brk 1, pr]]) qs))),
    4.14 -                Pretty.brk 1, Pretty.str "in ", pu,
    4.15 -                Pretty.brk 1, Pretty.str "end"])) pargs)
    4.16 +                Pretty.brk 1, Codegen.str "in ", pu,
    4.17 +                Pretty.brk 1, Codegen.str "end"])) pargs)
    4.18            end
    4.19      end
    4.20    | _ => NONE);
    4.21 @@ -1029,8 +1029,8 @@
    4.22                 (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
    4.23             in
    4.24               SOME (gr2, Codegen.mk_app brack
    4.25 -               (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
    4.26 -                 Pretty.brk 1, pu, Pretty.str ")"]) pargs)
    4.27 +               (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
    4.28 +                 Pretty.brk 1, pu, Codegen.str ")"]) pargs)
    4.29             end
    4.30         | _ => NONE)
    4.31    | _ => NONE);
     5.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri May 23 16:37:57 2008 +0200
     5.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri May 23 16:41:39 2008 +0200
     5.3 @@ -62,23 +62,23 @@
     5.4              val (gr''', rest) = mk_dtdef gr'' "and " xs
     5.5            in
     5.6              (gr''',
     5.7 -             Pretty.block (Pretty.str prfx ::
     5.8 +             Pretty.block (str prfx ::
     5.9                 (if null tvs then [] else
    5.10 -                  [mk_tuple (map Pretty.str tvs), Pretty.str " "]) @
    5.11 -               [Pretty.str (type_id ^ " ="), Pretty.brk 1] @
    5.12 -               List.concat (separate [Pretty.brk 1, Pretty.str "| "]
    5.13 +                  [mk_tuple (map str tvs), str " "]) @
    5.14 +               [str (type_id ^ " ="), Pretty.brk 1] @
    5.15 +               List.concat (separate [Pretty.brk 1, str "| "]
    5.16                   (map (fn (ps', (_, cname)) => [Pretty.block
    5.17 -                   (Pretty.str cname ::
    5.18 +                   (str cname ::
    5.19                      (if null ps' then [] else
    5.20 -                     List.concat ([Pretty.str " of", Pretty.brk 1] ::
    5.21 -                       separate [Pretty.str " *", Pretty.brk 1]
    5.22 +                     List.concat ([str " of", Pretty.brk 1] ::
    5.23 +                       separate [str " *", Pretty.brk 1]
    5.24                           (map single ps'))))]) ps))) :: rest)
    5.25            end;
    5.26  
    5.27      fun mk_constr_term cname Ts T ps =
    5.28 -      List.concat (separate [Pretty.str " $", Pretty.brk 1]
    5.29 -        ([Pretty.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
    5.30 -          mk_type false (Ts ---> T), Pretty.str ")"] :: ps));
    5.31 +      List.concat (separate [str " $", Pretty.brk 1]
    5.32 +        ([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
    5.33 +          mk_type false (Ts ---> T), str ")"] :: ps));
    5.34  
    5.35      fun mk_term_of_def gr prfx [] = []
    5.36        | mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) =
    5.37 @@ -89,14 +89,14 @@
    5.38              val rest = mk_term_of_def gr "and " xs;
    5.39              val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) =>
    5.40                let val args = map (fn i =>
    5.41 -                Pretty.str ("x" ^ string_of_int i)) (1 upto length Ts)
    5.42 +                str ("x" ^ string_of_int i)) (1 upto length Ts)
    5.43                in ("  | ", Pretty.blk (4,
    5.44 -                [Pretty.str prfx, mk_term_of gr module' false T, Pretty.brk 1,
    5.45 -                 if null Ts then Pretty.str (snd (get_const_id cname gr))
    5.46 +                [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
    5.47 +                 if null Ts then str (snd (get_const_id cname gr))
    5.48                   else parens (Pretty.block
    5.49 -                   [Pretty.str (snd (get_const_id cname gr)),
    5.50 +                   [str (snd (get_const_id cname gr)),
    5.51                      Pretty.brk 1, mk_tuple args]),
    5.52 -                 Pretty.str " =", Pretty.brk 1] @
    5.53 +                 str " =", Pretty.brk 1] @
    5.54                   mk_constr_term cname Ts T
    5.55                     (map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U,
    5.56                        Pretty.brk 1, x]]) (args ~~ Ts))))
    5.57 @@ -114,20 +114,20 @@
    5.58              val SOME (cname, _) = find_nonempty descr [i] i;
    5.59  
    5.60              fun mk_delay p = Pretty.block
    5.61 -              [Pretty.str "fn () =>", Pretty.brk 1, p];
    5.62 +              [str "fn () =>", Pretty.brk 1, p];
    5.63  
    5.64 -            fun mk_force p = Pretty.block [p, Pretty.brk 1, Pretty.str "()"];
    5.65 +            fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"];
    5.66  
    5.67              fun mk_constr s b (cname, dts) =
    5.68                let
    5.69                  val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s
    5.70                      (DatatypeAux.typ_of_dtyp descr sorts dt))
    5.71 -                  [Pretty.str (if b andalso DatatypeAux.is_rec_type dt then "0"
    5.72 +                  [str (if b andalso DatatypeAux.is_rec_type dt then "0"
    5.73                       else "j")]) dts;
    5.74                  val Ts = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
    5.75 -                val xs = map Pretty.str
    5.76 +                val xs = map str
    5.77                    (DatatypeProp.indexify_names (replicate (length dts) "x"));
    5.78 -                val ts = map Pretty.str
    5.79 +                val ts = map str
    5.80                    (DatatypeProp.indexify_names (replicate (length dts) "t"));
    5.81                  val (_, id) = get_const_id cname gr
    5.82                in
    5.83 @@ -136,52 +136,52 @@
    5.84                    (mk_tuple
    5.85                      [case xs of
    5.86                         _ :: _ :: _ => Pretty.block
    5.87 -                         [Pretty.str id, Pretty.brk 1, mk_tuple xs]
    5.88 -                     | _ => mk_app false (Pretty.str id) xs,
    5.89 +                         [str id, Pretty.brk 1, mk_tuple xs]
    5.90 +                     | _ => mk_app false (str id) xs,
    5.91                       mk_delay (Pretty.block (mk_constr_term cname Ts T
    5.92                         (map (single o mk_force) ts)))])
    5.93                end;
    5.94  
    5.95              fun mk_choice [c] = mk_constr "(i-1)" false c
    5.96 -              | mk_choice cs = Pretty.block [Pretty.str "one_of",
    5.97 -                  Pretty.brk 1, Pretty.blk (1, Pretty.str "[" ::
    5.98 -                  List.concat (separate [Pretty.str ",", Pretty.fbrk]
    5.99 +              | mk_choice cs = Pretty.block [str "one_of",
   5.100 +                  Pretty.brk 1, Pretty.blk (1, str "[" ::
   5.101 +                  List.concat (separate [str ",", Pretty.fbrk]
   5.102                      (map (single o mk_delay o mk_constr "(i-1)" false) cs)) @
   5.103 -                  [Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"];
   5.104 +                  [str "]"]), Pretty.brk 1, str "()"];
   5.105  
   5.106              val gs = maps (fn s =>
   5.107                let val s' = strip_tname s
   5.108 -              in [Pretty.str (s' ^ "G"), Pretty.str (s' ^ "T")] end) tvs;
   5.109 +              in [str (s' ^ "G"), str (s' ^ "T")] end) tvs;
   5.110              val gen_name = "gen_" ^ snd (get_type_id tname gr)
   5.111  
   5.112            in
   5.113              Pretty.blk (4, separate (Pretty.brk 1) 
   5.114 -                (Pretty.str (prfx ^ gen_name ^
   5.115 +                (str (prfx ^ gen_name ^
   5.116                     (if null cs1 then "" else "'")) :: gs @
   5.117 -                 (if null cs1 then [] else [Pretty.str "i"]) @
   5.118 -                 [Pretty.str "j"]) @
   5.119 -              [Pretty.str " =", Pretty.brk 1] @
   5.120 +                 (if null cs1 then [] else [str "i"]) @
   5.121 +                 [str "j"]) @
   5.122 +              [str " =", Pretty.brk 1] @
   5.123                (if not (null cs1) andalso not (null cs2)
   5.124 -               then [Pretty.str "frequency", Pretty.brk 1,
   5.125 -                 Pretty.blk (1, [Pretty.str "[",
   5.126 -                   mk_tuple [Pretty.str "i", mk_delay (mk_choice cs1)],
   5.127 -                   Pretty.str ",", Pretty.fbrk,
   5.128 -                   mk_tuple [Pretty.str "1", mk_delay (mk_choice cs2)],
   5.129 -                   Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"]
   5.130 +               then [str "frequency", Pretty.brk 1,
   5.131 +                 Pretty.blk (1, [str "[",
   5.132 +                   mk_tuple [str "i", mk_delay (mk_choice cs1)],
   5.133 +                   str ",", Pretty.fbrk,
   5.134 +                   mk_tuple [str "1", mk_delay (mk_choice cs2)],
   5.135 +                   str "]"]), Pretty.brk 1, str "()"]
   5.136                 else if null cs2 then
   5.137 -                 [Pretty.block [Pretty.str "(case", Pretty.brk 1,
   5.138 -                   Pretty.str "i", Pretty.brk 1, Pretty.str "of",
   5.139 -                   Pretty.brk 1, Pretty.str "0 =>", Pretty.brk 1,
   5.140 +                 [Pretty.block [str "(case", Pretty.brk 1,
   5.141 +                   str "i", Pretty.brk 1, str "of",
   5.142 +                   Pretty.brk 1, str "0 =>", Pretty.brk 1,
   5.143                     mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
   5.144 -                   Pretty.brk 1, Pretty.str "| _ =>", Pretty.brk 1,
   5.145 -                   mk_choice cs1, Pretty.str ")"]]
   5.146 +                   Pretty.brk 1, str "| _ =>", Pretty.brk 1,
   5.147 +                   mk_choice cs1, str ")"]]
   5.148                 else [mk_choice cs2])) ::
   5.149              (if null cs1 then []
   5.150               else [Pretty.blk (4, separate (Pretty.brk 1) 
   5.151 -                 (Pretty.str ("and " ^ gen_name) :: gs @ [Pretty.str "i"]) @
   5.152 -               [Pretty.str " =", Pretty.brk 1] @
   5.153 -               separate (Pretty.brk 1) (Pretty.str (gen_name ^ "'") :: gs @
   5.154 -                 [Pretty.str "i", Pretty.str "i"]))]) @
   5.155 +                 (str ("and " ^ gen_name) :: gs @ [str "i"]) @
   5.156 +               [str " =", Pretty.brk 1] @
   5.157 +               separate (Pretty.brk 1) (str (gen_name ^ "'") :: gs @
   5.158 +                 [str "i", str "i"]))]) @
   5.159              mk_gen_of_def gr "and " xs
   5.160            end
   5.161  
   5.162 @@ -194,15 +194,15 @@
   5.163             val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr';
   5.164           in
   5.165             map_node node_id (K (NONE, module',
   5.166 -             Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
   5.167 -               [Pretty.str ";"])) ^ "\n\n" ^
   5.168 +             string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
   5.169 +               [str ";"])) ^ "\n\n" ^
   5.170               (if "term_of" mem !mode then
   5.171 -                Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
   5.172 -                  (mk_term_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
   5.173 +                string_of (Pretty.blk (0, separate Pretty.fbrk
   5.174 +                  (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   5.175                else "") ^
   5.176               (if "test" mem !mode then
   5.177 -                Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
   5.178 -                  (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
   5.179 +                string_of (Pretty.blk (0, separate Pretty.fbrk
   5.180 +                  (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   5.181                else ""))) gr2
   5.182           end,
   5.183       module')
   5.184 @@ -236,17 +236,17 @@
   5.185                  val (gr1, p) = invoke_codegen thy defs dep module false (gr0, t');
   5.186                  val (ps, gr2) = pcase gr1 cs ts Us;
   5.187                in
   5.188 -                ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2)
   5.189 +                ([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2)
   5.190                end;
   5.191  
   5.192          val (ps1, gr1) = pcase gr constrs ts1 Ts;
   5.193 -        val ps = List.concat (separate [Pretty.brk 1, Pretty.str "| "] ps1);
   5.194 +        val ps = List.concat (separate [Pretty.brk 1, str "| "] ps1);
   5.195          val (gr2, p) = invoke_codegen thy defs dep module false (gr1, t);
   5.196          val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep module true) (gr2, ts2)
   5.197        in (gr3, (if not (null ts2) andalso brack then parens else I)
   5.198          (Pretty.block (separate (Pretty.brk 1)
   5.199 -          (Pretty.block ([Pretty.str "(case ", p, Pretty.str " of",
   5.200 -             Pretty.brk 1] @ ps @ [Pretty.str ")"]) :: ps2))))
   5.201 +          (Pretty.block ([str "(case ", p, str " of",
   5.202 +             Pretty.brk 1] @ ps @ [str ")"]) :: ps2))))
   5.203        end
   5.204    end;
   5.205  
   5.206 @@ -264,8 +264,8 @@
   5.207             (invoke_codegen thy defs dep module (i = 1)) (gr, ts);
   5.208         in (case args of
   5.209            _ :: _ :: _ => (gr', (if brack then parens else I)
   5.210 -            (Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps]))
   5.211 -        | _ => (gr', mk_app brack (Pretty.str id) ps))
   5.212 +            (Pretty.block [str id, Pretty.brk 1, mk_tuple ps]))
   5.213 +        | _ => (gr', mk_app brack (str id) ps))
   5.214         end
   5.215    end;
   5.216  
   5.217 @@ -304,8 +304,8 @@
   5.218               val (gr''', tyid) = mk_type_id module' s gr''
   5.219             in SOME (gr''',
   5.220               Pretty.block ((if null Ts then [] else
   5.221 -               [mk_tuple ps, Pretty.str " "]) @
   5.222 -               [Pretty.str (mk_qual_id module tyid)]))
   5.223 +               [mk_tuple ps, str " "]) @
   5.224 +               [str (mk_qual_id module tyid)]))
   5.225             end)
   5.226    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   5.227  
     6.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri May 23 16:37:57 2008 +0200
     6.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri May 23 16:41:39 2008 +0200
     6.3 @@ -260,12 +260,12 @@
     6.4  
     6.5  fun mk_eq (x::xs) =
     6.6    let fun mk_eqs _ [] = []
     6.7 -        | mk_eqs a (b::cs) = Pretty.str (a ^ " = " ^ b) :: mk_eqs b cs
     6.8 +        | mk_eqs a (b::cs) = str (a ^ " = " ^ b) :: mk_eqs b cs
     6.9    in mk_eqs x xs end;
    6.10  
    6.11 -fun mk_tuple xs = Pretty.block (Pretty.str "(" ::
    6.12 -  List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
    6.13 -  [Pretty.str ")"]);
    6.14 +fun mk_tuple xs = Pretty.block (str "(" ::
    6.15 +  List.concat (separate [str ",", Pretty.brk 1] (map single xs)) @
    6.16 +  [str ")"]);
    6.17  
    6.18  fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
    6.19        NONE => ((names, (s, [s])::vs), s)
    6.20 @@ -287,18 +287,18 @@
    6.21    | is_exhaustive _ = false;
    6.22  
    6.23  fun compile_match nvs eq_ps out_ps success_p can_fail =
    6.24 -  let val eqs = List.concat (separate [Pretty.str " andalso", Pretty.brk 1]
    6.25 +  let val eqs = List.concat (separate [str " andalso", Pretty.brk 1]
    6.26      (map single (List.concat (map (mk_eq o snd) nvs) @ eq_ps)));
    6.27    in
    6.28      Pretty.block
    6.29 -     ([Pretty.str "(fn ", mk_tuple out_ps, Pretty.str " =>", Pretty.brk 1] @
    6.30 -      (Pretty.block ((if eqs=[] then [] else Pretty.str "if " ::
    6.31 -         [Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @
    6.32 +     ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @
    6.33 +      (Pretty.block ((if eqs=[] then [] else str "if " ::
    6.34 +         [Pretty.block eqs, Pretty.brk 1, str "then "]) @
    6.35           (success_p ::
    6.36 -          (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else DSeq.empty"]))) ::
    6.37 +          (if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
    6.38         (if can_fail then
    6.39 -          [Pretty.brk 1, Pretty.str "| _ => DSeq.empty)"]
    6.40 -        else [Pretty.str ")"])))
    6.41 +          [Pretty.brk 1, str "| _ => DSeq.empty)"]
    6.42 +        else [str ")"])))
    6.43    end;
    6.44  
    6.45  fun modename module s (iss, is) gr =
    6.46 @@ -310,14 +310,14 @@
    6.47    end;
    6.48  
    6.49  fun mk_funcomp brack s k p = (if brack then parens else I)
    6.50 -  (Pretty.block [Pretty.block ((if k = 0 then [] else [Pretty.str "("]) @
    6.51 -    separate (Pretty.brk 1) (Pretty.str s :: replicate k (Pretty.str "|> ???")) @
    6.52 -    (if k = 0 then [] else [Pretty.str ")"])), Pretty.brk 1, p]);
    6.53 +  (Pretty.block [Pretty.block ((if k = 0 then [] else [str "("]) @
    6.54 +    separate (Pretty.brk 1) (str s :: replicate k (str "|> ???")) @
    6.55 +    (if k = 0 then [] else [str ")"])), Pretty.brk 1, p]);
    6.56  
    6.57  fun compile_expr thy defs dep module brack modes (gr, (NONE, t)) =
    6.58        apsnd single (invoke_codegen thy defs dep module brack (gr, t))
    6.59    | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
    6.60 -      (gr, [Pretty.str name])
    6.61 +      (gr, [str name])
    6.62    | compile_expr thy defs dep module brack modes (gr, (SOME (Mode (mode, _, ms)), t)) =
    6.63        (case strip_comb t of
    6.64           (Const (name, _), args) =>
    6.65 @@ -328,13 +328,13 @@
    6.66                     (compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>>
    6.67                   modename module name mode;
    6.68                 val (gr'', ps') = (case mode of
    6.69 -                   ([], []) => (gr', [Pretty.str "()"])
    6.70 +                   ([], []) => (gr', [str "()"])
    6.71                   | _ => foldl_map
    6.72                       (invoke_codegen thy defs dep module true) (gr', args2))
    6.73               in (gr', (if brack andalso not (null ps andalso null ps') then
    6.74                 single o parens o Pretty.block else I)
    6.75                   (List.concat (separate [Pretty.brk 1]
    6.76 -                   ([Pretty.str mode_id] :: ps @ map single ps'))))
    6.77 +                   ([str mode_id] :: ps @ map single ps'))))
    6.78               end
    6.79             else apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
    6.80               (invoke_codegen thy defs dep module true (gr, t))
    6.81 @@ -353,7 +353,7 @@
    6.82          in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
    6.83  
    6.84      fun compile_eq (gr, (s, t)) =
    6.85 -      apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
    6.86 +      apsnd (Pretty.block o cons (str (s ^ " = ")) o single)
    6.87          (invoke_codegen thy defs dep module false (gr, t));
    6.88  
    6.89      val (in_ts, out_ts) = get_args is 1 ts;
    6.90 @@ -374,7 +374,7 @@
    6.91              val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
    6.92            in
    6.93              (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
    6.94 -              (Pretty.block [Pretty.str "DSeq.single", Pretty.brk 1, mk_tuple out_ps])
    6.95 +              (Pretty.block [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps])
    6.96                (exists (not o is_exhaustive) out_ts'''))
    6.97            end
    6.98        | compile_prems out_ts vs names gr ps =
    6.99 @@ -405,13 +405,13 @@
   6.100                           (compile_expr thy defs dep module false modes
   6.101                             (gr2, (mode, t)))
   6.102                       else
   6.103 -                       apsnd (fn p => [Pretty.str "DSeq.of_list", Pretty.brk 1, p])
   6.104 +                       apsnd (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
   6.105                             (invoke_codegen thy defs dep module true (gr2, t));
   6.106                     val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
   6.107                   in
   6.108                     (gr4, compile_match (snd nvs) eq_ps out_ps
   6.109                        (Pretty.block (ps @
   6.110 -                         [Pretty.str " :->", Pretty.brk 1, rest]))
   6.111 +                         [str " :->", Pretty.brk 1, rest]))
   6.112                        (exists (not o is_exhaustive) out_ts''))
   6.113                   end
   6.114               | Sidecond t =>
   6.115 @@ -420,21 +420,21 @@
   6.116                     val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
   6.117                   in
   6.118                     (gr3, compile_match (snd nvs) eq_ps out_ps
   6.119 -                      (Pretty.block [Pretty.str "?? ", side_p,
   6.120 -                        Pretty.str " :->", Pretty.brk 1, rest])
   6.121 +                      (Pretty.block [str "?? ", side_p,
   6.122 +                        str " :->", Pretty.brk 1, rest])
   6.123                        (exists (not o is_exhaustive) out_ts''))
   6.124                   end)
   6.125            end;
   6.126  
   6.127      val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps;
   6.128    in
   6.129 -    (gr', Pretty.block [Pretty.str "DSeq.single", Pretty.brk 1, inp,
   6.130 -       Pretty.str " :->", Pretty.brk 1, prem_p])
   6.131 +    (gr', Pretty.block [str "DSeq.single", Pretty.brk 1, inp,
   6.132 +       str " :->", Pretty.brk 1, prem_p])
   6.133    end;
   6.134  
   6.135  fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode =
   6.136    let
   6.137 -    val xs = map Pretty.str (Name.variant_list arg_vs
   6.138 +    val xs = map str (Name.variant_list arg_vs
   6.139        (map (fn i => "x" ^ string_of_int i) (snd mode)));
   6.140      val (gr', (cl_ps, mode_id)) =
   6.141        foldl_map (fn (gr, cl) => compile_clause thy defs
   6.142 @@ -443,12 +443,12 @@
   6.143    in
   6.144      ((gr', "and "), Pretty.block
   6.145        ([Pretty.block (separate (Pretty.brk 1)
   6.146 -         (Pretty.str (prfx ^ mode_id) ::
   6.147 -           map Pretty.str arg_vs @
   6.148 -           (case mode of ([], []) => [Pretty.str "()"] | _ => xs)) @
   6.149 -         [Pretty.str " ="]),
   6.150 +         (str (prfx ^ mode_id) ::
   6.151 +           map str arg_vs @
   6.152 +           (case mode of ([], []) => [str "()"] | _ => xs)) @
   6.153 +         [str " ="]),
   6.154          Pretty.brk 1] @
   6.155 -       List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
   6.156 +       List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))))
   6.157    end;
   6.158  
   6.159  fun compile_preds thy defs gr dep module all_vs arg_vs modes preds =
   6.160 @@ -457,7 +457,7 @@
   6.161        dep module prfx' all_vs arg_vs modes s cls mode)
   6.162          ((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds)
   6.163    in
   6.164 -    (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
   6.165 +    (gr', space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n")
   6.166    end;
   6.167  
   6.168  (**** processing of introduction rules ****)
   6.169 @@ -605,11 +605,11 @@
   6.170        val (gr', (fun_id, mode_id)) = gr |>
   6.171          mk_const_id module' name |>>>
   6.172          modename module' pname ([], mode);
   6.173 -      val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode;
   6.174 -      val s = Pretty.string_of (Pretty.block
   6.175 -        [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =",
   6.176 -         Pretty.brk 1, Pretty.str "DSeq.hd", Pretty.brk 1,
   6.177 -         parens (Pretty.block (separate (Pretty.brk 1) (Pretty.str mode_id ::
   6.178 +      val vars = map (fn i => str ("x" ^ string_of_int i)) mode;
   6.179 +      val s = string_of (Pretty.block
   6.180 +        [mk_app false (str ("fun " ^ snd fun_id)) vars, str " =",
   6.181 +         Pretty.brk 1, str "DSeq.hd", Pretty.brk 1,
   6.182 +         parens (Pretty.block (separate (Pretty.brk 1) (str mode_id ::
   6.183             vars)))]) ^ ";\n\n";
   6.184        val gr'' = mk_ind_def thy defs (add_edge (name, dep)
   6.185          (new_node (name, (NONE, module', s)) gr')) name [pname] module'
   6.186 @@ -626,7 +626,7 @@
   6.187  fun conv_ntuple fs ts p =
   6.188    let
   6.189      val k = length fs;
   6.190 -    val xs = map (fn i => Pretty.str ("x" ^ string_of_int i)) (0 upto k);
   6.191 +    val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k);
   6.192      val xs' = map (fn Bound i => nth xs (k - i)) ts;
   6.193      fun conv xs js =
   6.194        if js mem fs then
   6.195 @@ -638,9 +638,9 @@
   6.196    in
   6.197      if k > 0 then
   6.198        Pretty.block
   6.199 -        [Pretty.str "DSeq.map (fn", Pretty.brk 1,
   6.200 -         mk_tuple xs', Pretty.str " =>", Pretty.brk 1, fst (conv xs []),
   6.201 -         Pretty.str ")", Pretty.brk 1, parens p]
   6.202 +        [str "DSeq.map (fn", Pretty.brk 1,
   6.203 +         mk_tuple xs', str " =>", Pretty.brk 1, fst (conv xs []),
   6.204 +         str ")", Pretty.brk 1, parens p]
   6.205      else p
   6.206    end;
   6.207  
   6.208 @@ -664,8 +664,8 @@
   6.209                      let val (gr', call_p) = mk_ind_call thy defs gr dep module true
   6.210                        s T (ts1 @ ts2') names thyname k intrs
   6.211                      in SOME (gr', (if brack then parens else I) (Pretty.block
   6.212 -                      [Pretty.str "DSeq.list_of", Pretty.brk 1, Pretty.str "(",
   6.213 -                       conv_ntuple fs ots call_p, Pretty.str ")"]))
   6.214 +                      [str "DSeq.list_of", Pretty.brk 1, str "(",
   6.215 +                       conv_ntuple fs ots call_p, str ")"]))
   6.216                      end
   6.217                    else NONE
   6.218                  end
   6.219 @@ -690,7 +690,7 @@
   6.220              dep module (if_library thyname module) gr;
   6.221            val (gr'', ps) = foldl_map
   6.222              (invoke_codegen thy defs dep module true) (gr', ts);
   6.223 -        in SOME (gr'', mk_app brack (Pretty.str id) ps)
   6.224 +        in SOME (gr'', mk_app brack (str id) ps)
   6.225          end)
   6.226    | _ => NONE);
   6.227  
     7.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri May 23 16:37:57 2008 +0200
     7.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri May 23 16:41:39 2008 +0200
     7.3 @@ -105,13 +105,13 @@
     7.4          val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs);
     7.5          val (gr3, rest) = mk_fundef module fname' false gr2 xs
     7.6        in
     7.7 -        (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  | " else prfx),
     7.8 -           pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
     7.9 +        (gr3, Pretty.blk (4, [str (if fname = fname' then "  | " else prfx),
    7.10 +           pl, str " =", Pretty.brk 1, pr]) :: rest)
    7.11        end;
    7.12  
    7.13      fun put_code module fundef = map_node dname
    7.14 -      (K (SOME (EQN ("", dummyT, dname)), module, Pretty.string_of (Pretty.blk (0,
    7.15 -      separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
    7.16 +      (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
    7.17 +      separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
    7.18  
    7.19    in
    7.20      (case try (get_node gr) dname of
    7.21 @@ -162,7 +162,7 @@
    7.22              add_rec_funs thy defs gr' dep (map prop_of eqns) module';
    7.23            val (gr''', fname) = mk_const_id module'' (s ^ suffix) gr''
    7.24          in
    7.25 -          SOME (gr''', mk_app brack (Pretty.str (mk_qual_id module fname)) ps)
    7.26 +          SOME (gr''', mk_app brack (str (mk_qual_id module fname)) ps)
    7.27          end)
    7.28    | _ => NONE);
    7.29  
     8.1 --- a/src/HOL/Tools/typedef_codegen.ML	Fri May 23 16:37:57 2008 +0200
     8.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Fri May 23 16:41:39 2008 +0200
     8.3 @@ -23,7 +23,7 @@
     8.4          val (gr'', ps) =
     8.5            foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
     8.6          val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
     8.7 -      in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
     8.8 +      in SOME (gr'', Codegen.mk_app brack (Codegen.str id) ps) end;
     8.9      fun lookup f T =
    8.10        (case TypedefPackage.get_info thy (get_name T) of
    8.11          NONE => ""
    8.12 @@ -41,8 +41,8 @@
    8.13       | _ => NONE)
    8.14    end;
    8.15  
    8.16 -fun mk_tyexpr [] s = Pretty.str s
    8.17 -  | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
    8.18 +fun mk_tyexpr [] s = Codegen.str s
    8.19 +  | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
    8.20    | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    8.21  
    8.22  fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    8.23 @@ -69,31 +69,31 @@
    8.24                     (Codegen.add_edge (node_id, dep)
    8.25                        (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
    8.26                   val s =
    8.27 -                   Pretty.string_of (Pretty.block [Pretty.str "datatype ",
    8.28 +                   Codegen.string_of (Pretty.block [Codegen.str "datatype ",
    8.29                       mk_tyexpr ps (snd ty_id),
    8.30 -                     Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
    8.31 -                     Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
    8.32 -                   Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
    8.33 -                     Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    8.34 -                     Pretty.str "x) = x;"]) ^ "\n\n" ^
    8.35 +                     Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
    8.36 +                     Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
    8.37 +                   Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
    8.38 +                     Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
    8.39 +                     Codegen.str "x) = x;"]) ^ "\n\n" ^
    8.40                     (if "term_of" mem !Codegen.mode then
    8.41 -                      Pretty.string_of (Pretty.block [Pretty.str "fun ",
    8.42 +                      Codegen.string_of (Pretty.block [Codegen.str "fun ",
    8.43                          Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
    8.44 -                        Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    8.45 -                        Pretty.str "x) =", Pretty.brk 1,
    8.46 -                        Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
    8.47 +                        Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
    8.48 +                        Codegen.str "x) =", Pretty.brk 1,
    8.49 +                        Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
    8.50                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    8.51 -                          Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
    8.52 +                          Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
    8.53                          Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
    8.54 -                        Pretty.str "x;"]) ^ "\n\n"
    8.55 +                        Codegen.str "x;"]) ^ "\n\n"
    8.56                      else "") ^
    8.57                     (if "test" mem !Codegen.mode then
    8.58 -                      Pretty.string_of (Pretty.block [Pretty.str "fun ",
    8.59 +                      Codegen.string_of (Pretty.block [Codegen.str "fun ",
    8.60                          Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
    8.61 -                        Pretty.str "i =", Pretty.brk 1,
    8.62 -                        Pretty.block [Pretty.str (Abs_id ^ " ("),
    8.63 +                        Codegen.str "i =", Pretty.brk 1,
    8.64 +                        Pretty.block [Codegen.str (Abs_id ^ " ("),
    8.65                            Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
    8.66 -                          Pretty.str "i);"]]) ^ "\n\n"
    8.67 +                          Codegen.str "i);"]]) ^ "\n\n"
    8.68                      else "")
    8.69                 in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
    8.70               | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)