src/Tools/Code/code_scala.ML

     val deresolve_tyco = deresolve o Type_Constructor;
     val deresolve_class = deresolve o Type_Class;
     fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true;
     fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs);
     fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
-          (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
+          (print_typ tyvars NOBR) fxy ((Pretty.str o deresolve) sym) tys
     and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
          of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys)
           | SOME (_, print) => print (print_typ tyvars) fxy tys)
-      | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
+      | print_typ tyvars fxy (ITyVar v) = (Pretty.str o lookup_tyvar tyvars) v;
     fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]);
     fun print_tupled_typ tyvars ([], ty) =
           print_typ tyvars NOBR ty
       | print_tupled_typ tyvars ([ty1], ty2) =
-          concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
+          concat [print_typ tyvars BR ty1, Pretty.str "=>", print_typ tyvars NOBR ty2]
       | print_tupled_typ tyvars (tys, ty) =
-          concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
-            str "=>", print_typ tyvars NOBR ty];
-    fun constraint p1 p2 = Pretty.block [p1, str " : ", p2];
-    fun print_var vars NONE = str "_"
-      | print_var vars (SOME v) = (str o lookup_var vars) v;
+          concat [Pretty.enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
+            Pretty.str "=>", print_typ tyvars NOBR ty];
+    fun constraint p1 p2 = Pretty.block [p1, Pretty.str " : ", p2];
+    fun print_var vars NONE = Pretty.str "_"
+      | print_var vars (SOME v) = (Pretty.str o lookup_var vars) v;
     fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d
     and applify_plain_dict tyvars (Dict_Const (inst, dss)) =
-          applify_dictss tyvars ((str o deresolve o Class_Instance) inst) (map snd dss)
+          applify_dictss tyvars ((Pretty.str o deresolve o Class_Instance) inst) (map snd dss)
       | applify_plain_dict tyvars (Dict_Var { var, class, ... }) =
-          Pretty.block [str "implicitly",
-            enclose "[" "]" [Pretty.block [(str o deresolve_class) class,
-              enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]]
+          Pretty.block [Pretty.str "implicitly",
+            Pretty.enclose "[" "]" [Pretty.block [(Pretty.str o deresolve_class) class,
+              Pretty.enclose "[" "]" [(Pretty.str o lookup_tyvar tyvars) var]]]]
     and applify_dictss tyvars p dss =
       applify "(" ")" (applify_dict tyvars) NOBR p (flat dss)
     fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
           print_app tyvars is_pat some_thm vars fxy (const, [])
       | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =

     and print_abs_head tyvars (some_v, ty) vars =
            let
              val vars' = intro_vars (the_list some_v) vars;
            in
              (concat [
-               enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)],
-               str "=>"
+               Pretty.enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)],
+               Pretty.str "=>"
              ], vars')
            end
     and print_app tyvars is_pat some_thm vars fxy
         (app as (const as { sym, typargs, dom, dicts, ... }, ts)) =
       let

         val (wanted, print') = case syntax of
             NONE => (args_num sym, fn fxy => fn ts => applify_dicts
               (gen_applify (is_constr sym) "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR ((str o deresolve) sym) typargs') ts) dicts)
+                  NOBR ((Pretty.str o deresolve) sym) typargs') ts) dicts)
           | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts
               (applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR (str s) typargs') ts) dicts)
+                  NOBR (Pretty.str s) typargs') ts) dicts)
           | SOME (k, Complex_printer print) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
                 (ts ~~ take k dom))
         val ((vs_tys, (ts1, rty)), ts2) =
           Code_Thingol.satisfied_application wanted app;

         if null vs_tys then
           if null ts2 then
             print' fxy ts
           else
             Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
-              [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts2)
+              [Pretty.str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, Pretty.str ")"]) ts2)
         else
           print_term tyvars is_pat some_thm vars fxy (vs_tys `|==> (IConst const `$$ ts1, rty))
       end
     and print_bind tyvars some_thm fxy p =
       gen_print_bind (print_term tyvars true) some_thm fxy p
     and print_case tyvars some_thm vars fxy { clauses = [], ... } =
-          (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"]
+          (brackify fxy o Pretty.breaks o map Pretty.str) ["sys.error(\"empty case\")"]
       | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
           let
             val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
             fun print_match_val ((pat, ty), t) vars =
               vars
               |> print_bind tyvars some_thm BR pat
-              |>> (fn p => (false, concat [str "val", p, str "=",
+              |>> (fn p => (false, concat [Pretty.str "val", p, Pretty.str "=",
                 constraint (print_term tyvars false some_thm vars NOBR t) (print_typ tyvars BR ty)]));
             fun print_match_seq t vars =
               ((true, print_term tyvars false some_thm vars NOBR t), vars);
             fun print_match is_first ((IVar NONE, ty), t) =
                   if Code_Thingol.is_IAbs t andalso is_first

             val (seps_ps, vars') =
               vars |> print_match true bind ||>> fold_map (print_match false) binds |>> uncurry cons;
             val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)];
             fun insert_seps [(_, p)] = [p]
               | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
-                  (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
-          in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
+                  (if sep then Pretty.block [p, Pretty.str ";"] else p) :: insert_seps seps_ps
+          in brackify_block fxy (Pretty.str "{") (insert_seps all_seps_ps) (Pretty.str "}") end
       | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
           let
             fun print_select (pat, body) =
               let
                 val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
                 val p_body = print_term tyvars false some_thm vars' NOBR body
-              in concat [str "case", p_pat, str "=>", p_body] end;
+              in concat [Pretty.str "case", p_pat, Pretty.str "=>", p_body] end;
           in
             map print_select clauses
-            |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match {"], str "}")
+            |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, Pretty.str "match {"], Pretty.str "}")
             |> single
-            |> enclose "(" ")"
+            |> Pretty.enclose "(" ")"
           end;
     fun print_context tyvars vs s = applify "[" "]"
-      (fn (v, sort) => (Pretty.block o map str)
+      (fn (v, sort) => (Pretty.block o map Pretty.str)
         (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
-          NOBR (str s) vs;
+          NOBR (Pretty.str s) vs;
     fun print_defhead tyvars vars const vs params tys ty =
-      concat [str "def", constraint (applify "(" ")" (fn (param, ty) =>
-        constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
+      concat [Pretty.str "def", constraint (applify "(" ")" (fn (param, ty) =>
+        constraint ((Pretty.str o lookup_var vars) param) (print_typ tyvars NOBR ty))
           NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
-            str "="];
+            Pretty.str "="];
     fun print_def const (vs, ty) [] =
           let
             val (tys, ty') = Code_Thingol.unfold_fun ty;
             val params = Name.invent (snd reserved) "a" (length tys);
             val tyvars = intro_tyvars vs reserved;
             val vars = intro_vars params reserved;
           in
             concat [print_defhead tyvars vars const vs params tys ty',
-              str ("sys.error(" ^ print_scala_string const ^ ")")]
+              Pretty.str ("sys.error(" ^ print_scala_string const ^ ")")]
           end
       | print_def const (vs, ty) eqs =
           let
             val tycos = build (fold (fn ((ts, t), _) =>
               fold Code_Thingol.add_tyconames (t :: ts)) eqs);

               then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
               else aux_params vars1 (map (fst o fst) eqs);
             val vars2 = intro_vars params vars1;
             val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
             fun tuplify [p] = p
-              | tuplify ps = enum "," "(" ")" ps;
+              | tuplify ps = Pretty.enum "," "(" ")" ps;
             fun print_rhs vars' ((_, t), (some_thm, _)) =
               print_term tyvars false some_thm vars' NOBR t;
             fun print_clause (eq as ((ts, _), (some_thm, _))) =
               let
                 val vars' =
                   intro_vars (build (fold Code_Thingol.add_varnames ts)) vars1;
               in
-                concat [str "case",
+                concat [Pretty.str "case",
                   tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
-                  str "=>", print_rhs vars' eq]
+                  Pretty.str "=>", print_rhs vars' eq]
               end;
             val head = print_defhead tyvars vars2 const vs params tys' ty';
           in if simple then
             concat [head, print_rhs vars2 (hd eqs)]
           else
             Pretty.block_enclose
-              (concat [head, tuplify (map (str o lookup_var vars2) params),
-                str "match {"], str "}")
+              (concat [head, tuplify (map (Pretty.str o lookup_var vars2) params),
+                Pretty.str "match {"], Pretty.str "}")
               (map print_clause eqs)
           end;
-    val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
+    val print_method = Pretty.str o enclose "`" "`" o deresolve_full o Constant;
     fun print_inst class (tyco, { vs, inst_params, superinst_params }) =
       let
         val tyvars = intro_tyvars vs reserved;
         val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
         fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) =

             val aux_dom = Name.invent_names (snd reserved) "a" dom;
             val auxs = map fst aux_dom;
             val vars = intro_vars auxs reserved;
             val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
             fun abstract_using [] = []
-              | abstract_using aux_dom = [enum "," "(" ")"
-                  (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
-                  (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+              | abstract_using aux_dom = [Pretty.enum "," "(" ")"
+                  (map (fn (aux, ty) => constraint ((Pretty.str o lookup_var vars) aux)
+                  (print_typ tyvars NOBR ty)) aux_dom), Pretty.str "=>"];
             val aux_abstr1 = abstract_using aux_dom1;
             val aux_abstr2 = abstract_using aux_dom2;
           in
-            concat ([str "val", print_method classparam, str "="]
+            concat ([Pretty.str "val", print_method classparam, Pretty.str "="]
               @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
                 (const, map (IVar o SOME) auxs))
           end;
       in
-        Pretty.block_enclose (concat [str "implicit def",
+        Pretty.block_enclose (concat [Pretty.str "implicit def",
           constraint (print_context tyvars vs
             ((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class)))
           (print_dicttyp tyvars classtyp),
-          str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
+          Pretty.str "=", Pretty.str "new", print_dicttyp tyvars classtyp, Pretty.str "{"], Pretty.str "}")
             (map print_classparam_instance (inst_params @ superinst_params))
       end;
     fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) =
           print_def const (vs, ty) (filter (snd o snd) raw_eqs)
       | print_stmt (Type_Constructor tyco, (_, Datatype (vs, cos))) =
           let
             val tyvars = intro_tyvars (map (rpair []) vs) reserved;
             fun print_co ((co, vs_args), tys) =
-              concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
-                (str ("final case class " ^ deresolve_const co)) vs_args)
-                @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
+              concat [Pretty.block ((applify "[" "]" (Pretty.str o lookup_tyvar tyvars) NOBR
+                (Pretty.str ("final case class " ^ deresolve_const co)) vs_args)
+                @@ Pretty.enum "," "(" ")" (map (fn (v, arg) => constraint (Pretty.str v) (print_typ tyvars NOBR arg))
                   (Name.invent_names (snd reserved) "a" tys))),
-                str "extends",
-                applify "[" "]" (str o lookup_tyvar tyvars) NOBR
-                  ((str o deresolve_tyco) tyco) vs
+                Pretty.str "extends",
+                applify "[" "]" (Pretty.str o lookup_tyvar tyvars) NOBR
+                  ((Pretty.str o deresolve_tyco) tyco) vs
               ];
           in
-            Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
-              NOBR (str ("abstract sealed class " ^ deresolve_tyco tyco)) vs
+            Pretty.chunks (applify "[" "]" (Pretty.str o lookup_tyvar tyvars)
+              NOBR (Pretty.str ("abstract sealed class " ^ deresolve_tyco tyco)) vs
                 :: map print_co cos)
           end
       | print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) =
           let
             val tyvars = intro_tyvars [(v, [class])] reserved;
             fun add_typarg s = Pretty.block
-              [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
+              [Pretty.str s, Pretty.str "[", (Pretty.str o lookup_tyvar tyvars) v, Pretty.str "]"];
             fun print_super_classes [] = NONE
-              | print_super_classes classrels = SOME (concat (str "extends"
-                  :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels)));
+              | print_super_classes classrels = SOME (concat (Pretty.str "extends"
+                  :: separate (Pretty.str "with") (map (add_typarg o deresolve_class o snd) classrels)));
             fun print_classparam_val (classparam, ty) =
-              concat [str "val", constraint (print_method classparam)
+              concat [Pretty.str "val", constraint (print_method classparam)
                 ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
             fun print_classparam_def (classparam, ty) =
               let
                 val (tys, ty) = Code_Thingol.unfold_fun ty;
                 val [implicit_name] = Name.invent (snd reserved) (lookup_tyvar tyvars v) 1;
                 val proto_vars = intro_vars [implicit_name] reserved;
                 val auxs = Name.invent (snd proto_vars) "a" (length tys);
                 val vars = intro_vars auxs proto_vars;
               in
-                concat [str "def", constraint (Pretty.block [applify "(" ")"
-                  (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+                concat [Pretty.str "def", constraint (Pretty.block [applify "(" ")"
+                  (fn (aux, ty) => constraint ((Pretty.str o lookup_var vars) aux)
                   (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
-                  (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
-                  add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=",
-                  applify "(" ")" (str o lookup_var vars) NOBR
-                  (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
+                  (auxs ~~ tys), Pretty.str "(implicit ", Pretty.str implicit_name, Pretty.str ": ",
+                  add_typarg (deresolve_class class), Pretty.str ")"]) (print_typ tyvars NOBR ty), Pretty.str "=",
+                  applify "(" ")" (Pretty.str o lookup_var vars) NOBR
+                  (Pretty.block [Pretty.str implicit_name, Pretty.str ".", print_method classparam]) auxs]
               end;
           in
             Pretty.chunks (
               (Pretty.block_enclose
-                (concat ([str "trait", (add_typarg o deresolve_class) class]
-                  @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
+                (concat ([Pretty.str "trait", (add_typarg o deresolve_class) class]
+                  @ the_list (print_super_classes classrels) @ [Pretty.str "{"]), Pretty.str "}")
                 (map print_classparam_val classparams))
               :: map print_classparam_def classparams
               @| Pretty.block_enclose
-                (str ("object " ^ deresolve_class class ^ " {"), str "}")
+                (Pretty.str ("object " ^ deresolve_class class ^ " {"), Pretty.str "}")
                 (map (print_inst class) insts)
             )
           end;
   in print_stmt end;
 

       tyco_syntax const_syntax (make_vars reserved_syms) args_num
       (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []);
 
     (* print modules *)
     fun print_module _ base _ ps = Pretty.chunks2
-      (str ("object " ^ base ^ " {")
-        :: ps @| str ("} /* object " ^ base ^ " */"));
+      (Pretty.str ("object " ^ base ^ " {")
+        :: ps @| Pretty.str ("} /* object " ^ base ^ " */"));
 
     (* serialization *)
     val p = Pretty.chunks2 (map snd includes
       @ Code_Namespace.print_hierarchical {
         print_module = print_module, print_stmt = print_stmt,

     then signed_string_of_int k
     else quote (signed_string_of_int k)
 in Literals {
   literal_string = print_scala_string,
   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
-  literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
+  literal_list = fn [] => Pretty.str "Nil" | ps => Pretty.block [Pretty.str "List", Pretty.enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;
 
 
 (** Isar setup **)

       evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"})
   #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ BR ty1 (*product type vs. tupled arguments!*),
-        str "=>",
+        Pretty.str "=>",
         print_typ (INFX (1, R)) ty2
       )))]))
   #> fold (Code_Target.add_reserved target) [
       "abstract", "case", "catch", "class", "def", "do", "else", "enum", "export", "extends",
       "false", "final", "finally", "for", "forSome", "given", "if", "implicit", "import", "lazy",