# HG changeset patch # User wenzelm # Date 1537810454 -7200 # Node ID 56c6378ebaeabaa892f2147b4edaadee13217fdb # Parent bc4cc763b0eab39ff0dcaad56af433f3ccd5a070 tuned signature: prefer value-oriented pretty-printing; diff -r bc4cc763b0ea -r 56c6378ebaea src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Mon Sep 24 19:06:56 2018 +0200 +++ b/src/Pure/Isar/expression.ML Mon Sep 24 19:34:14 2018 +0200 @@ -44,7 +44,7 @@ (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context (* Diagnostic *) - val print_dependencies: Proof.context -> bool -> expression -> unit + val pretty_dependencies: Proof.context -> bool -> expression -> Pretty.T end; structure Expression : EXPRESSION = @@ -875,12 +875,10 @@ of the expression in the current context (clean = false) or in an empty context (clean = true). **) -fun print_dependencies ctxt clean expression = +fun pretty_dependencies ctxt clean expression = let val ((_, _, deps, _, export), expr_ctxt) = read_goal_expression expression ctxt; val export' = if clean then Morphism.identity else export; - in - Locale.print_dependencies expr_ctxt clean export' deps - end; + in Locale.pretty_dependencies expr_ctxt clean export' deps end; end; diff -r bc4cc763b0ea -r 56c6378ebaea src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Sep 24 19:06:56 2018 +0200 +++ b/src/Pure/Isar/locale.ML Mon Sep 24 19:34:14 2018 +0200 @@ -87,10 +87,9 @@ (* Diagnostic *) val get_locales: theory -> string list val print_locales: bool -> theory -> unit - val print_locale: theory -> bool -> xstring * Position.T -> unit + val pretty_locale: theory -> bool -> string -> Pretty.T val print_registrations: Proof.context -> xstring * Position.T -> unit - val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit - val pretty_locale: theory -> bool -> string -> Pretty.T list + val pretty_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> Pretty.T val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list end; @@ -723,13 +722,10 @@ |> tap consolidate_notes |> map force_notes; in - Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name :: - maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems + Pretty.block (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name :: + maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems) end; -fun print_locale thy show_facts raw_name = - Pretty.writeln (Pretty.block (pretty_locale thy show_facts (check thy raw_name))); - fun print_registrations ctxt raw_name = let val thy = Proof_Context.theory_of ctxt; @@ -740,7 +736,7 @@ | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs))) end |> Pretty.writeln; -fun print_dependencies ctxt clean export insts = +fun pretty_dependencies ctxt clean export insts = let val thy = Proof_Context.theory_of ctxt; val idents = if clean then empty_idents else Idents.get (Context.Proof ctxt); @@ -748,14 +744,14 @@ (case fold (roundup thy cons export) insts (idents, []) |> snd of [] => Pretty.str "no dependencies" | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt export) (rev deps))) - end |> Pretty.writeln; + end; fun pretty_locale_deps thy = let fun make_node name = {name = name, parents = map (fst o fst) (dependencies_of thy name), - body = Pretty.block (pretty_locale thy false name)}; + body = pretty_locale thy false name}; val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []); in map make_node names end; diff -r bc4cc763b0ea -r 56c6378ebaea src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Mon Sep 24 19:06:56 2018 +0200 +++ b/src/Pure/Isar/named_target.ML Mon Sep 24 19:34:14 2018 +0200 @@ -104,8 +104,7 @@ declaration = Generic_Target.locale_declaration locale, theory_registration = fn _ => error "Not possible in locale target", locale_dependency = Generic_Target.locale_dependency locale, - pretty = fn ctxt => - [Pretty.block (Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale)]} + pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]} | operations (Class class) = {define = Generic_Target.define (class_foundation class), notes = Generic_Target.notes (Generic_Target.locale_target_notes class), diff -r bc4cc763b0ea -r 56c6378ebaea src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Sep 24 19:06:56 2018 +0200 +++ b/src/Pure/Pure.thy Mon Sep 24 19:34:14 2018 +0200 @@ -1108,8 +1108,12 @@ val _ = Outer_Syntax.command \<^command_keyword>\print_locale\ "print locale of this theory" - (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) => - Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name))); + (Parse.opt_bang -- Parse.position Parse.name >> (fn (show_facts, raw_name) => + Toplevel.keep (fn state => + let + val thy = Toplevel.theory_of state; + val name = Locale.check thy raw_name; + in Pretty.writeln (Locale.pretty_locale thy show_facts name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_interps\ @@ -1120,8 +1124,9 @@ val _ = Outer_Syntax.command \<^command_keyword>\print_dependencies\ "print dependencies of locale expression" - (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) => - Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr))); + (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (clean, expr) => + Toplevel.keep (fn state => + Pretty.writeln (Expression.pretty_dependencies (Toplevel.context_of state) clean expr)))); val _ = Outer_Syntax.command \<^command_keyword>\print_attributes\