Pretty.chunks;

--- a/src/HOL/Tools/inductive_package.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -79,9 +79,9 @@
     Library.generic_merge Thm.eq_thm I I monos1 monos2);
 
   fun print sg (tab, monos) =
-    (Pretty.writeln (Pretty.strs ("(co)inductives:" ::
-       map #1 (Sign.cond_extern_table sg Sign.constK tab)));
-     Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)));
+    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
+     Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
+    |> Pretty.chunks |> Pretty.writeln;
 end;
 
 structure InductiveData = TheoryDataFun(InductiveArgs);

--- a/src/HOL/Tools/record_package.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -379,7 +379,10 @@
       fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks
         (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
           pretty_parent parent @ map pretty_field fields));
-    in seq (Pretty.writeln o pretty_record) (Sign.cond_extern_table sg Sign.typeK recs) end;
+    in
+      map pretty_record (Sign.cond_extern_table sg Sign.typeK recs)
+      |> Pretty.chunks |> Pretty.writeln
+    end;
 end;
 
 structure RecordsData = TheoryDataFun(RecordsArgs);

--- a/src/Pure/Isar/attrib.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -15,7 +15,7 @@
 signature ATTRIB =
 sig
   include BASIC_ATTRIB
-  val help_attributes: theory option -> unit
+  val help_attributes: theory option -> Pretty.T list
   exception ATTRIB_FAIL of (string * Position.T) * exn
   val global_attribute: theory -> Args.src -> theory attribute
   val local_attribute: theory -> Args.src -> Proof.context attribute
@@ -62,25 +62,23 @@
       attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups =>
         error ("Attempt to merge different versions of attributes " ^ commas_quote dups)};
 
-  fun print_atts verbose ({space, attrs}) =
+  fun pretty_atts verbose ({space, attrs}) =
     let
       fun prt_attr (name, ((_, comment), _)) = Pretty.block
         [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     in
-      if not verbose then ()
-      else Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
-      Pretty.writeln (Pretty.big_list "attributes:"
-        (map prt_attr (NameSpace.cond_extern_table space attrs)))
+      (if not verbose then [] else [Display.pretty_name_space ("attribute name space", space)]) @
+      [Pretty.big_list "attributes:" (map prt_attr (NameSpace.cond_extern_table space attrs))]
     end;
 
-   fun print _ = print_atts true;
+   fun print _ = Pretty.writeln o Pretty.chunks o pretty_atts true;
 end;
 
 structure AttributesData = TheoryDataFun(AttributesDataArgs);
 val print_attributes = AttributesData.print;
 
-fun help_attributes None = writeln "attributes: (unkown theory context)"
-  | help_attributes (Some thy) = AttributesDataArgs.print_atts false (AttributesData.get thy);
+fun help_attributes None = [Pretty.str "attributes: (unkown theory context)"]
+  | help_attributes (Some thy) = AttributesDataArgs.pretty_atts false (AttributesData.get thy);
 
 
 (* get global / local attributes *)

--- a/src/Pure/Isar/method.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/Pure/Isar/method.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -52,7 +52,7 @@
   val set_tactic: (Proof.context -> thm list -> tactic) -> unit
   val tactic: string -> Proof.context -> Proof.method
   exception METHOD_FAIL of (string * Position.T) * exn
-  val help_methods: theory option -> unit
+  val help_methods: theory option -> Pretty.T list
   val method: theory -> Args.src -> Proof.context -> Proof.method
   val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
     -> theory -> theory
@@ -373,25 +373,23 @@
       meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups =>
         error ("Attempt to merge different versions of methods " ^ commas_quote dups)};
 
-  fun print_meths verbose {space, meths} =
+  fun pretty_meths verbose {space, meths} =
     let
       fun prt_meth (name, ((_, comment), _)) = Pretty.block
         [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     in
-      if not verbose then ()
-      else Pretty.writeln (Display.pretty_name_space ("method name space", space));
-      Pretty.writeln (Pretty.big_list "methods:"
-        (map prt_meth (NameSpace.cond_extern_table space meths)))
+      (if not verbose then [] else [Display.pretty_name_space ("method name space", space)]) @
+      [Pretty.big_list "methods:" (map prt_meth (NameSpace.cond_extern_table space meths))]
     end;
 
-  fun print _ = print_meths true;
+  fun print _ = Pretty.writeln o Pretty.chunks o pretty_meths true;
 end;
 
 structure MethodsData = TheoryDataFun(MethodsDataArgs);
 val print_methods = MethodsData.print;
 
-fun help_methods None = writeln "methods: (unkown theory context)"
-  | help_methods (Some thy) = MethodsDataArgs.print_meths false (MethodsData.get thy);
+fun help_methods None = [Pretty.str "methods: (unkown theory context)"]
+  | help_methods (Some thy) = MethodsDataArgs.pretty_meths false (MethodsData.get thy);
 
 
 (* get methods *)

--- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -205,24 +205,26 @@
   map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only))
     (Symtab.dest (get_parsers ()));
 
-fun print_outer_syntax () =
+fun help_outer_syntax () =
   let
     fun pretty_cmd (name, comment, _, _) =
       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     val (int_cmds, cmds) = partition #4 (dest_parsers ());
   in
-    Pretty.writeln (Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())));
-    Pretty.writeln (Pretty.big_list "proper commands:" (map pretty_cmd cmds));
-    Pretty.writeln (Pretty.big_list "improper commands (interactive-only):"
-      (map pretty_cmd int_cmds))
+    [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
+      Pretty.big_list "proper commands:" (map pretty_cmd cmds),
+      Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)]
   end;
 
+val print_outer_syntax = Pretty.writeln o Pretty.chunks o help_outer_syntax;
+
 val print_help =
   Toplevel.keep (fn state =>
     let val opt_thy = try Toplevel.theory_of state in
-      print_outer_syntax ();
-      Method.help_methods opt_thy;
+      help_outer_syntax () @
+      Method.help_methods opt_thy @
       Attrib.help_attributes opt_thy
+      |> Pretty.chunks |> Pretty.writeln
     end);
 
 

--- a/src/Pure/Syntax/syntax.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -281,10 +281,11 @@
     val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
     val prmodes' = sort_strings (filter_out (equal "") prmodes);
   in
-    Pretty.writeln (pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon));
-    Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
-    Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram));
-    Pretty.writeln (pretty_strs_qs "print modes:" prmodes')
+    [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
+      Pretty.strs ("logtypes:" :: logtypes),
+      Pretty.big_list "prods:" (Parser.pretty_gram gram),
+      pretty_strs_qs "print modes:" prmodes']
+    |> Pretty.chunks |> Pretty.writeln
   end;
 
 
@@ -303,14 +304,15 @@
     val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
       print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
   in
-    Pretty.writeln (pretty_strs_qs "consts:" consts);
-    Pretty.writeln (pretty_trtab "parse_ast_translation:" parse_ast_trtab);
-    Pretty.writeln (pretty_ruletab "parse_rules:" parse_ruletab);
-    Pretty.writeln (pretty_trtab "parse_translation:" parse_trtab);
-    Pretty.writeln (pretty_trtab "print_translation:" print_trtab);
-    Pretty.writeln (pretty_ruletab "print_rules:" print_ruletab);
-    Pretty.writeln (pretty_trtab "print_ast_translation:" print_ast_trtab);
-    Pretty.writeln (Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab))
+    [pretty_strs_qs "consts:" consts,
+      pretty_trtab "parse_ast_translation:" parse_ast_trtab,
+      pretty_ruletab "parse_rules:" parse_ruletab,
+      pretty_trtab "parse_translation:" parse_trtab,
+      pretty_trtab "print_translation:" print_trtab,
+      pretty_ruletab "print_rules:" print_ruletab,
+      pretty_trtab "print_ast_translation:" print_ast_trtab,
+      Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
+    |> Pretty.chunks |> Pretty.writeln
   end;
 
 
@@ -425,7 +427,7 @@
 
     fun constify (ast as Ast.Constant _) = ast
       | constify (ast as Ast.Variable x) =
-          if x mem consts orelse NameSpace.qualified x then Ast.Constant x
+          if x mem consts orelse NameSpace.is_qualified x then Ast.Constant x
           else ast
       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   in

--- a/src/Pure/axclass.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/Pure/axclass.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -193,7 +193,7 @@
 
       fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks
         [pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
-    in seq (Pretty.writeln o pretty_axclass) (Symtab.dest tab) end;
+    in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
 end;
 
 structure AxclassesData = TheoryDataFun(AxclassesArgs);

--- a/src/Pure/display.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/Pure/display.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -31,7 +31,7 @@
   val pretty_theory	: theory -> Pretty.T
   val pprint_theory	: theory -> pprint_args -> unit
   val print_syntax	: theory -> unit
-  val print_theory	: theory -> unit
+  val pretty_full_theory: theory -> Pretty.T list
   val pretty_name_space : string * NameSpace.T -> Pretty.T
   val show_consts	: bool ref
 end;
@@ -155,15 +155,17 @@
 
 
 
-(* print signature *)
+(* print theory *)
 
-fun print_sign sg =
+fun pretty_full_theory thy =
   let
+    val sg = Theory.sign_of thy;
+
     fun prt_cls c = Sign.pretty_sort sg [c];
     fun prt_sort S = Sign.pretty_sort sg S;
     fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]);
     fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty);
-
+    fun prt_term t = Pretty.quote (Sign.pretty_term sg t);
 
     fun pretty_classes cs = Pretty.block
       (Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs));
@@ -195,47 +197,37 @@
     fun pretty_const (c, ty) = Pretty.block
       [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
 
+    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
+
+
     val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
+    val {axioms, oracles, ...} = Theory.rep_theory thy;
     val spaces' = Library.sort_wrt fst spaces;
     val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
       Type.rep_tsig tsig;
     val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
     val consts = Sign.cond_extern_table sg Sign.constK const_tab;
+    val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
+    val oras = Sign.cond_extern_table sg Theory.oracleK oracles;
   in
-    Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
-    Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data));
-    Pretty.writeln (Pretty.strs ["name prefix:", NameSpace.pack path]);
-    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
-    Pretty.writeln (pretty_classes classes);
-    Pretty.writeln (Pretty.big_list "class relation:"
-      (map pretty_classrel (Symtab.dest classrel)));
-    Pretty.writeln (pretty_default default);
-    Pretty.writeln (pretty_log_types log_types);
-    Pretty.writeln (pretty_witness univ_witness);
-    Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
-    Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)));
-    Pretty.writeln (Pretty.big_list "type arities:"
-      (flat (map pretty_arities (Symtab.dest arities))));
-    Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts))
+    [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
+      Pretty.strs ("data:" :: Sign.data_kinds data),
+      Pretty.strs ["name prefix:", NameSpace.pack path],
+      Pretty.big_list "name spaces:" (map pretty_name_space spaces'),
+      pretty_classes classes,
+      Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)),
+      pretty_default default,
+      pretty_log_types log_types,
+      pretty_witness univ_witness,
+      Pretty.big_list "type constructors:" (map pretty_ty tycons),
+      Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)),
+      Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
+      Pretty.big_list "consts:" (map pretty_const consts),
+      Pretty.big_list "axioms:" (map prt_axm axms),
+      Pretty.strs ("oracles:" :: (map #1 oras))]
   end;
 
 
-(* print axioms, oracles, theorems *)
-
-fun print_thy thy =
-  let
-    val {sign, axioms, oracles, ...} = Theory.rep_theory thy;
-    fun cond_externs kind = Sign.cond_extern_table sign kind;
-
-    fun prt_axm (a, t) = Pretty.block
-      [Pretty.str (a ^ ":"), Pretty.brk 1, Pretty.quote (Sign.pretty_term sign t)];
-  in
-    Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm (cond_externs Theory.axiomK axioms)));
-    Pretty.writeln (Pretty.strs ("oracles:" :: (map #1 (cond_externs Theory.oracleK oracles))))
-  end;
-
-fun print_theory thy = (print_sign (Theory.sign_of thy); print_thy thy);
-
 (*also show consts in case of showing types?*)
 val show_consts = ref false;
 

--- a/src/Pure/locale.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/Pure/locale.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -129,9 +129,10 @@
       val locs = map (apfst extrn) (Symtab.dest locales);
       val scope_names = rev (map (extrn o fst) (! scope));
     in
-      Pretty.writeln (Display.pretty_name_space ("locale name space", space));
-      Pretty.writeln (Pretty.big_list "locales:" (map (pretty_locale sg) locs));
-      Pretty.writeln (Pretty.strs ("current scope:" :: scope_names))
+      [Display.pretty_name_space ("locale name space", space),
+        Pretty.big_list "locales:" (map (pretty_locale sg) locs),
+        Pretty.strs ("current scope:" :: scope_names)]
+      |> Pretty.chunks |> Pretty.writeln
     end;
 end;
 

--- a/src/Pure/pure_thy.ML	Sat Apr 15 17:41:20 2000 +0200
+++ b/src/Pure/pure_thy.ML	Mon Apr 17 13:57:55 2000 +0200
@@ -78,7 +78,7 @@
   val prep_ext = mk_empty;
   val merge = mk_empty;
 
-  fun print sg (ref {space, thms_tab, const_idx = _}) =
+  fun pretty sg (ref {space, thms_tab, const_idx = _}) =
     let
       val prt_thm = Display.pretty_thm o Thm.transfer_sg sg;
       fun prt_thms (name, [th]) =
@@ -87,9 +87,11 @@
 
       val thmss = NameSpace.cond_extern_table space thms_tab;
     in
-      Pretty.writeln (Display.pretty_name_space ("theorem name space", space));
-      Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
+      [Display.pretty_name_space ("theorem name space", space),
+        Pretty.big_list "theorems:" (map prt_thms thmss)]
     end;
+
+  fun print sg data = Pretty.writeln (Pretty.chunks (pretty sg data));
 end;
 
 structure TheoremsData = TheoryDataFun(TheoremsDataArgs);
@@ -102,8 +104,10 @@
 (* print theory *)
 
 val print_theorems = TheoremsData.print;
+
 fun print_theory thy =
-  (Display.print_theory thy; print_theorems thy);
+  Display.pretty_full_theory thy @ TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)
+  |> Pretty.chunks |> Pretty.writeln;