# HG changeset patch # User wenzelm # Date 955972675 -7200 # Node ID 840c75ab2a7f5dafae9c2086205a8de89601c1ed # Parent 8ffa2c825fd79036b01d07b7d71e3f7f58ca130d Pretty.chunks; diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/HOL/Tools/inductive_package.ML --- 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); diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/HOL/Tools/record_package.ML --- 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); diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/Pure/Isar/attrib.ML --- 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 *) diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/Pure/Isar/method.ML --- 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 *) diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/Pure/Isar/outer_syntax.ML --- 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); diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/Pure/Syntax/syntax.ML --- 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 diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/Pure/axclass.ML --- 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); diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/Pure/display.ML --- 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; diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/Pure/locale.ML --- 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; diff -r 8ffa2c825fd7 -r 840c75ab2a7f src/Pure/pure_thy.ML --- 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;