src/HOL/Tools/record.ML

   val split_simproc: (term -> int) -> simproc
   val ex_sel_eq_simproc: simproc
   val split_tac: Proof.context -> int -> tactic
   val split_simp_tac: Proof.context -> thm list -> (term -> int) -> int -> tactic
   val split_wrapper: string * (Proof.context -> wrapper)
+
+  val pretty_recT: Proof.context -> typ -> Pretty.T
+  val string_of_record: Proof.context -> string -> string
 
   val codegen: bool Config.T
   val updateN: string
   val ext_typeN: string
   val extN: string

   in thy |> add_record overloaded (params', binding) parent fields end;
 
 end;
 
 
+(* printing *)
+
+local
+
+fun the_parent_recT (Type (parent, [Type (_, [unit as Type (_,[])])])) = Type (parent, [unit])
+  | the_parent_recT (Type (extT, [T])) = Type (extT, [the_parent_recT T])
+  | the_parent_recT T = raise TYPE ("Not a unit record scheme with parent: ", [T], [])
+
+in
+
+fun pretty_recT ctxt typ =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val (fs, (_, moreT)) = get_recT_fields thy typ
+    val _ = if moreT = HOLogic.unitT then () else raise TYPE ("Not a unit record scheme: ", [typ], [])
+    val parent = if length (dest_recTs typ) >= 2 then SOME (the_parent_recT typ) else NONE
+    val pfs = case parent of SOME p => fst (get_recT_fields thy p) | NONE => []
+    val fs' = drop (length pfs) fs
+    fun pretty_field (name, typ) = Pretty.block [
+          Syntax.pretty_term ctxt (Const (name, typ)),
+          Pretty.brk 1,
+          Pretty.str "::",
+          Pretty.brk 1,
+          Syntax.pretty_typ ctxt typ
+        ]
+  in
+    Pretty.block (Library.separate (Pretty.brk 1)
+      ([Pretty.keyword1 "record", Syntax.pretty_typ ctxt typ, Pretty.str "="] @
+        (case parent of
+          SOME p => [Syntax.pretty_typ ctxt p, Pretty.str "+"]
+        | NONE => [])) @
+      Pretty.fbrk ::
+      Pretty.fbreaks (map pretty_field fs'))
+  end
+
+end
+
+fun string_of_record ctxt s =
+  let
+    val T = Syntax.read_typ ctxt s
+  in
+    Pretty.string_of (pretty_recT ctxt T)
+      handle TYPE _ => error ("Unknown record: " ^ Syntax.string_of_typ ctxt T)
+  end
+
+val print_record =
+  let
+    fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
+         Print_Mode.with_modes modes (fn () => Output.writeln (string_of state arg)) ());
+  in print_item (string_of_record o Toplevel.context_of) end
+
+
 (* outer syntax *)
 
 val _ =
   Outer_Syntax.command @{command_keyword record} "define extensible record"
     (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) --
       (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
         Scan.repeat1 Parse.const_binding)
     >> (fn ((overloaded, x), (y, z)) =>
         Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
 
-end;
+val opt_modes =
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
+
+val _ =
+  Outer_Syntax.command @{command_keyword "print_record"} "print record definiton"
+    (opt_modes -- Parse.typ >> print_record);
+
+end