Pretty.chunks;
authorwenzelm
Mon Apr 17 13:57:55 2000 +0200 (2000-04-17)
changeset 8720840c75ab2a7f
parent 8719 8ffa2c825fd7
child 8721 453b493ece0a
Pretty.chunks;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Syntax/syntax.ML
src/Pure/axclass.ML
src/Pure/display.ML
src/Pure/locale.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Apr 15 17:41:20 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Apr 17 13:57:55 2000 +0200
     1.3 @@ -79,9 +79,9 @@
     1.4      Library.generic_merge Thm.eq_thm I I monos1 monos2);
     1.5  
     1.6    fun print sg (tab, monos) =
     1.7 -    (Pretty.writeln (Pretty.strs ("(co)inductives:" ::
     1.8 -       map #1 (Sign.cond_extern_table sg Sign.constK tab)));
     1.9 -     Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)));
    1.10 +    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
    1.11 +     Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
    1.12 +    |> Pretty.chunks |> Pretty.writeln;
    1.13  end;
    1.14  
    1.15  structure InductiveData = TheoryDataFun(InductiveArgs);
     2.1 --- a/src/HOL/Tools/record_package.ML	Sat Apr 15 17:41:20 2000 +0200
     2.2 +++ b/src/HOL/Tools/record_package.ML	Mon Apr 17 13:57:55 2000 +0200
     2.3 @@ -379,7 +379,10 @@
     2.4        fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks
     2.5          (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
     2.6            pretty_parent parent @ map pretty_field fields));
     2.7 -    in seq (Pretty.writeln o pretty_record) (Sign.cond_extern_table sg Sign.typeK recs) end;
     2.8 +    in
     2.9 +      map pretty_record (Sign.cond_extern_table sg Sign.typeK recs)
    2.10 +      |> Pretty.chunks |> Pretty.writeln
    2.11 +    end;
    2.12  end;
    2.13  
    2.14  structure RecordsData = TheoryDataFun(RecordsArgs);
     3.1 --- a/src/Pure/Isar/attrib.ML	Sat Apr 15 17:41:20 2000 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Mon Apr 17 13:57:55 2000 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4  signature ATTRIB =
     3.5  sig
     3.6    include BASIC_ATTRIB
     3.7 -  val help_attributes: theory option -> unit
     3.8 +  val help_attributes: theory option -> Pretty.T list
     3.9    exception ATTRIB_FAIL of (string * Position.T) * exn
    3.10    val global_attribute: theory -> Args.src -> theory attribute
    3.11    val local_attribute: theory -> Args.src -> Proof.context attribute
    3.12 @@ -62,25 +62,23 @@
    3.13        attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups =>
    3.14          error ("Attempt to merge different versions of attributes " ^ commas_quote dups)};
    3.15  
    3.16 -  fun print_atts verbose ({space, attrs}) =
    3.17 +  fun pretty_atts verbose ({space, attrs}) =
    3.18      let
    3.19        fun prt_attr (name, ((_, comment), _)) = Pretty.block
    3.20          [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    3.21      in
    3.22 -      if not verbose then ()
    3.23 -      else Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
    3.24 -      Pretty.writeln (Pretty.big_list "attributes:"
    3.25 -        (map prt_attr (NameSpace.cond_extern_table space attrs)))
    3.26 +      (if not verbose then [] else [Display.pretty_name_space ("attribute name space", space)]) @
    3.27 +      [Pretty.big_list "attributes:" (map prt_attr (NameSpace.cond_extern_table space attrs))]
    3.28      end;
    3.29  
    3.30 -   fun print _ = print_atts true;
    3.31 +   fun print _ = Pretty.writeln o Pretty.chunks o pretty_atts true;
    3.32  end;
    3.33  
    3.34  structure AttributesData = TheoryDataFun(AttributesDataArgs);
    3.35  val print_attributes = AttributesData.print;
    3.36  
    3.37 -fun help_attributes None = writeln "attributes: (unkown theory context)"
    3.38 -  | help_attributes (Some thy) = AttributesDataArgs.print_atts false (AttributesData.get thy);
    3.39 +fun help_attributes None = [Pretty.str "attributes: (unkown theory context)"]
    3.40 +  | help_attributes (Some thy) = AttributesDataArgs.pretty_atts false (AttributesData.get thy);
    3.41  
    3.42  
    3.43  (* get global / local attributes *)
     4.1 --- a/src/Pure/Isar/method.ML	Sat Apr 15 17:41:20 2000 +0200
     4.2 +++ b/src/Pure/Isar/method.ML	Mon Apr 17 13:57:55 2000 +0200
     4.3 @@ -52,7 +52,7 @@
     4.4    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
     4.5    val tactic: string -> Proof.context -> Proof.method
     4.6    exception METHOD_FAIL of (string * Position.T) * exn
     4.7 -  val help_methods: theory option -> unit
     4.8 +  val help_methods: theory option -> Pretty.T list
     4.9    val method: theory -> Args.src -> Proof.context -> Proof.method
    4.10    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
    4.11      -> theory -> theory
    4.12 @@ -373,25 +373,23 @@
    4.13        meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups =>
    4.14          error ("Attempt to merge different versions of methods " ^ commas_quote dups)};
    4.15  
    4.16 -  fun print_meths verbose {space, meths} =
    4.17 +  fun pretty_meths verbose {space, meths} =
    4.18      let
    4.19        fun prt_meth (name, ((_, comment), _)) = Pretty.block
    4.20          [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    4.21      in
    4.22 -      if not verbose then ()
    4.23 -      else Pretty.writeln (Display.pretty_name_space ("method name space", space));
    4.24 -      Pretty.writeln (Pretty.big_list "methods:"
    4.25 -        (map prt_meth (NameSpace.cond_extern_table space meths)))
    4.26 +      (if not verbose then [] else [Display.pretty_name_space ("method name space", space)]) @
    4.27 +      [Pretty.big_list "methods:" (map prt_meth (NameSpace.cond_extern_table space meths))]
    4.28      end;
    4.29  
    4.30 -  fun print _ = print_meths true;
    4.31 +  fun print _ = Pretty.writeln o Pretty.chunks o pretty_meths true;
    4.32  end;
    4.33  
    4.34  structure MethodsData = TheoryDataFun(MethodsDataArgs);
    4.35  val print_methods = MethodsData.print;
    4.36  
    4.37 -fun help_methods None = writeln "methods: (unkown theory context)"
    4.38 -  | help_methods (Some thy) = MethodsDataArgs.print_meths false (MethodsData.get thy);
    4.39 +fun help_methods None = [Pretty.str "methods: (unkown theory context)"]
    4.40 +  | help_methods (Some thy) = MethodsDataArgs.pretty_meths false (MethodsData.get thy);
    4.41  
    4.42  
    4.43  (* get methods *)
     5.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 15 17:41:20 2000 +0200
     5.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 17 13:57:55 2000 +0200
     5.3 @@ -205,24 +205,26 @@
     5.4    map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only))
     5.5      (Symtab.dest (get_parsers ()));
     5.6  
     5.7 -fun print_outer_syntax () =
     5.8 +fun help_outer_syntax () =
     5.9    let
    5.10      fun pretty_cmd (name, comment, _, _) =
    5.11        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    5.12      val (int_cmds, cmds) = partition #4 (dest_parsers ());
    5.13    in
    5.14 -    Pretty.writeln (Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())));
    5.15 -    Pretty.writeln (Pretty.big_list "proper commands:" (map pretty_cmd cmds));
    5.16 -    Pretty.writeln (Pretty.big_list "improper commands (interactive-only):"
    5.17 -      (map pretty_cmd int_cmds))
    5.18 +    [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
    5.19 +      Pretty.big_list "proper commands:" (map pretty_cmd cmds),
    5.20 +      Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)]
    5.21    end;
    5.22  
    5.23 +val print_outer_syntax = Pretty.writeln o Pretty.chunks o help_outer_syntax;
    5.24 +
    5.25  val print_help =
    5.26    Toplevel.keep (fn state =>
    5.27      let val opt_thy = try Toplevel.theory_of state in
    5.28 -      print_outer_syntax ();
    5.29 -      Method.help_methods opt_thy;
    5.30 +      help_outer_syntax () @
    5.31 +      Method.help_methods opt_thy @
    5.32        Attrib.help_attributes opt_thy
    5.33 +      |> Pretty.chunks |> Pretty.writeln
    5.34      end);
    5.35  
    5.36  
     6.1 --- a/src/Pure/Syntax/syntax.ML	Sat Apr 15 17:41:20 2000 +0200
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Apr 17 13:57:55 2000 +0200
     6.3 @@ -281,10 +281,11 @@
     6.4      val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
     6.5      val prmodes' = sort_strings (filter_out (equal "") prmodes);
     6.6    in
     6.7 -    Pretty.writeln (pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon));
     6.8 -    Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
     6.9 -    Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram));
    6.10 -    Pretty.writeln (pretty_strs_qs "print modes:" prmodes')
    6.11 +    [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
    6.12 +      Pretty.strs ("logtypes:" :: logtypes),
    6.13 +      Pretty.big_list "prods:" (Parser.pretty_gram gram),
    6.14 +      pretty_strs_qs "print modes:" prmodes']
    6.15 +    |> Pretty.chunks |> Pretty.writeln
    6.16    end;
    6.17  
    6.18  
    6.19 @@ -303,14 +304,15 @@
    6.20      val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
    6.21        print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
    6.22    in
    6.23 -    Pretty.writeln (pretty_strs_qs "consts:" consts);
    6.24 -    Pretty.writeln (pretty_trtab "parse_ast_translation:" parse_ast_trtab);
    6.25 -    Pretty.writeln (pretty_ruletab "parse_rules:" parse_ruletab);
    6.26 -    Pretty.writeln (pretty_trtab "parse_translation:" parse_trtab);
    6.27 -    Pretty.writeln (pretty_trtab "print_translation:" print_trtab);
    6.28 -    Pretty.writeln (pretty_ruletab "print_rules:" print_ruletab);
    6.29 -    Pretty.writeln (pretty_trtab "print_ast_translation:" print_ast_trtab);
    6.30 -    Pretty.writeln (Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab))
    6.31 +    [pretty_strs_qs "consts:" consts,
    6.32 +      pretty_trtab "parse_ast_translation:" parse_ast_trtab,
    6.33 +      pretty_ruletab "parse_rules:" parse_ruletab,
    6.34 +      pretty_trtab "parse_translation:" parse_trtab,
    6.35 +      pretty_trtab "print_translation:" print_trtab,
    6.36 +      pretty_ruletab "print_rules:" print_ruletab,
    6.37 +      pretty_trtab "print_ast_translation:" print_ast_trtab,
    6.38 +      Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
    6.39 +    |> Pretty.chunks |> Pretty.writeln
    6.40    end;
    6.41  
    6.42  
    6.43 @@ -425,7 +427,7 @@
    6.44  
    6.45      fun constify (ast as Ast.Constant _) = ast
    6.46        | constify (ast as Ast.Variable x) =
    6.47 -          if x mem consts orelse NameSpace.qualified x then Ast.Constant x
    6.48 +          if x mem consts orelse NameSpace.is_qualified x then Ast.Constant x
    6.49            else ast
    6.50        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
    6.51    in
     7.1 --- a/src/Pure/axclass.ML	Sat Apr 15 17:41:20 2000 +0200
     7.2 +++ b/src/Pure/axclass.ML	Mon Apr 17 13:57:55 2000 +0200
     7.3 @@ -193,7 +193,7 @@
     7.4  
     7.5        fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks
     7.6          [pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
     7.7 -    in seq (Pretty.writeln o pretty_axclass) (Symtab.dest tab) end;
     7.8 +    in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
     7.9  end;
    7.10  
    7.11  structure AxclassesData = TheoryDataFun(AxclassesArgs);
     8.1 --- a/src/Pure/display.ML	Sat Apr 15 17:41:20 2000 +0200
     8.2 +++ b/src/Pure/display.ML	Mon Apr 17 13:57:55 2000 +0200
     8.3 @@ -31,7 +31,7 @@
     8.4    val pretty_theory	: theory -> Pretty.T
     8.5    val pprint_theory	: theory -> pprint_args -> unit
     8.6    val print_syntax	: theory -> unit
     8.7 -  val print_theory	: theory -> unit
     8.8 +  val pretty_full_theory: theory -> Pretty.T list
     8.9    val pretty_name_space : string * NameSpace.T -> Pretty.T
    8.10    val show_consts	: bool ref
    8.11  end;
    8.12 @@ -155,15 +155,17 @@
    8.13  
    8.14  
    8.15  
    8.16 -(* print signature *)
    8.17 +(* print theory *)
    8.18  
    8.19 -fun print_sign sg =
    8.20 +fun pretty_full_theory thy =
    8.21    let
    8.22 +    val sg = Theory.sign_of thy;
    8.23 +
    8.24      fun prt_cls c = Sign.pretty_sort sg [c];
    8.25      fun prt_sort S = Sign.pretty_sort sg S;
    8.26      fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]);
    8.27      fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty);
    8.28 -
    8.29 +    fun prt_term t = Pretty.quote (Sign.pretty_term sg t);
    8.30  
    8.31      fun pretty_classes cs = Pretty.block
    8.32        (Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs));
    8.33 @@ -195,47 +197,37 @@
    8.34      fun pretty_const (c, ty) = Pretty.block
    8.35        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
    8.36  
    8.37 +    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    8.38 +
    8.39 +
    8.40      val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
    8.41 +    val {axioms, oracles, ...} = Theory.rep_theory thy;
    8.42      val spaces' = Library.sort_wrt fst spaces;
    8.43      val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
    8.44        Type.rep_tsig tsig;
    8.45      val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
    8.46      val consts = Sign.cond_extern_table sg Sign.constK const_tab;
    8.47 +    val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
    8.48 +    val oras = Sign.cond_extern_table sg Theory.oracleK oracles;
    8.49    in
    8.50 -    Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
    8.51 -    Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data));
    8.52 -    Pretty.writeln (Pretty.strs ["name prefix:", NameSpace.pack path]);
    8.53 -    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
    8.54 -    Pretty.writeln (pretty_classes classes);
    8.55 -    Pretty.writeln (Pretty.big_list "class relation:"
    8.56 -      (map pretty_classrel (Symtab.dest classrel)));
    8.57 -    Pretty.writeln (pretty_default default);
    8.58 -    Pretty.writeln (pretty_log_types log_types);
    8.59 -    Pretty.writeln (pretty_witness univ_witness);
    8.60 -    Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
    8.61 -    Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)));
    8.62 -    Pretty.writeln (Pretty.big_list "type arities:"
    8.63 -      (flat (map pretty_arities (Symtab.dest arities))));
    8.64 -    Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts))
    8.65 +    [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
    8.66 +      Pretty.strs ("data:" :: Sign.data_kinds data),
    8.67 +      Pretty.strs ["name prefix:", NameSpace.pack path],
    8.68 +      Pretty.big_list "name spaces:" (map pretty_name_space spaces'),
    8.69 +      pretty_classes classes,
    8.70 +      Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)),
    8.71 +      pretty_default default,
    8.72 +      pretty_log_types log_types,
    8.73 +      pretty_witness univ_witness,
    8.74 +      Pretty.big_list "type constructors:" (map pretty_ty tycons),
    8.75 +      Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)),
    8.76 +      Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
    8.77 +      Pretty.big_list "consts:" (map pretty_const consts),
    8.78 +      Pretty.big_list "axioms:" (map prt_axm axms),
    8.79 +      Pretty.strs ("oracles:" :: (map #1 oras))]
    8.80    end;
    8.81  
    8.82  
    8.83 -(* print axioms, oracles, theorems *)
    8.84 -
    8.85 -fun print_thy thy =
    8.86 -  let
    8.87 -    val {sign, axioms, oracles, ...} = Theory.rep_theory thy;
    8.88 -    fun cond_externs kind = Sign.cond_extern_table sign kind;
    8.89 -
    8.90 -    fun prt_axm (a, t) = Pretty.block
    8.91 -      [Pretty.str (a ^ ":"), Pretty.brk 1, Pretty.quote (Sign.pretty_term sign t)];
    8.92 -  in
    8.93 -    Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm (cond_externs Theory.axiomK axioms)));
    8.94 -    Pretty.writeln (Pretty.strs ("oracles:" :: (map #1 (cond_externs Theory.oracleK oracles))))
    8.95 -  end;
    8.96 -
    8.97 -fun print_theory thy = (print_sign (Theory.sign_of thy); print_thy thy);
    8.98 -
    8.99  (*also show consts in case of showing types?*)
   8.100  val show_consts = ref false;
   8.101  
     9.1 --- a/src/Pure/locale.ML	Sat Apr 15 17:41:20 2000 +0200
     9.2 +++ b/src/Pure/locale.ML	Mon Apr 17 13:57:55 2000 +0200
     9.3 @@ -129,9 +129,10 @@
     9.4        val locs = map (apfst extrn) (Symtab.dest locales);
     9.5        val scope_names = rev (map (extrn o fst) (! scope));
     9.6      in
     9.7 -      Pretty.writeln (Display.pretty_name_space ("locale name space", space));
     9.8 -      Pretty.writeln (Pretty.big_list "locales:" (map (pretty_locale sg) locs));
     9.9 -      Pretty.writeln (Pretty.strs ("current scope:" :: scope_names))
    9.10 +      [Display.pretty_name_space ("locale name space", space),
    9.11 +        Pretty.big_list "locales:" (map (pretty_locale sg) locs),
    9.12 +        Pretty.strs ("current scope:" :: scope_names)]
    9.13 +      |> Pretty.chunks |> Pretty.writeln
    9.14      end;
    9.15  end;
    9.16  
    10.1 --- a/src/Pure/pure_thy.ML	Sat Apr 15 17:41:20 2000 +0200
    10.2 +++ b/src/Pure/pure_thy.ML	Mon Apr 17 13:57:55 2000 +0200
    10.3 @@ -78,7 +78,7 @@
    10.4    val prep_ext = mk_empty;
    10.5    val merge = mk_empty;
    10.6  
    10.7 -  fun print sg (ref {space, thms_tab, const_idx = _}) =
    10.8 +  fun pretty sg (ref {space, thms_tab, const_idx = _}) =
    10.9      let
   10.10        val prt_thm = Display.pretty_thm o Thm.transfer_sg sg;
   10.11        fun prt_thms (name, [th]) =
   10.12 @@ -87,9 +87,11 @@
   10.13  
   10.14        val thmss = NameSpace.cond_extern_table space thms_tab;
   10.15      in
   10.16 -      Pretty.writeln (Display.pretty_name_space ("theorem name space", space));
   10.17 -      Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
   10.18 +      [Display.pretty_name_space ("theorem name space", space),
   10.19 +        Pretty.big_list "theorems:" (map prt_thms thmss)]
   10.20      end;
   10.21 +
   10.22 +  fun print sg data = Pretty.writeln (Pretty.chunks (pretty sg data));
   10.23  end;
   10.24  
   10.25  structure TheoremsData = TheoryDataFun(TheoremsDataArgs);
   10.26 @@ -102,8 +104,10 @@
   10.27  (* print theory *)
   10.28  
   10.29  val print_theorems = TheoremsData.print;
   10.30 +
   10.31  fun print_theory thy =
   10.32 -  (Display.print_theory thy; print_theorems thy);
   10.33 +  Display.pretty_full_theory thy @ TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)
   10.34 +  |> Pretty.chunks |> Pretty.writeln;
   10.35  
   10.36  
   10.37