tuned signature: prefer value-oriented pretty-printing;

--- 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;

--- 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;
 

--- 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),

--- 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>\<open>print_locale\<close>
     "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>\<open>print_interps\<close>
@@ -1120,8 +1124,9 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_dependencies\<close>
     "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>\<open>print_attributes\<close>