# HG changeset patch
# User wenzelm
# Date 1537811625 -7200
# Node ID 70f9826753f6255ebdc3007626796daf59b2db70
# Parent  f4fb93197670e17b7dc14075f1270526a2d61ac8
tuned signature: prefer value-oriented pretty-printing;

diff -r f4fb93197670 -r 70f9826753f6 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 19:43:20 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 19:53:45 2018 +0200
@@ -86,9 +86,9 @@
 
   (* Diagnostic *)
   val get_locales: theory -> string list
-  val print_locales: bool -> theory -> unit
+  val pretty_locales: theory -> bool -> Pretty.T
   val pretty_locale: theory -> bool -> string -> Pretty.T
-  val print_registrations: Proof.context -> xstring * Position.T -> unit
+  val pretty_registrations: Proof.context -> string -> Pretty.T
   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;
@@ -702,13 +702,12 @@
 
 fun get_locales thy = map #1 (Name_Space.dest_table (Locales.get thy));
 
-fun print_locales verbose thy =
+fun pretty_locales thy verbose =
   Pretty.block
     (Pretty.breaks
       (Pretty.str "locales:" ::
         map (Pretty.mark_str o #1)
-          (Name_Space.markup_table verbose (Proof_Context.init_global thy) (Locales.get thy))))
-  |> Pretty.writeln;
+          (Name_Space.markup_table verbose (Proof_Context.init_global thy) (Locales.get thy))));
 
 fun pretty_locale thy show_facts name =
   let
@@ -726,15 +725,10 @@
       maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems)
   end;
 
-fun print_registrations ctxt raw_name =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val name = check thy raw_name;
-  in
-    (case registrations_of (Context.Proof ctxt) name of
-      [] => Pretty.str "no interpretations"
-    | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs)))
-  end |> Pretty.writeln;
+fun pretty_registrations ctxt name =
+  (case registrations_of (Context.Proof ctxt) name of
+    [] => Pretty.str "no interpretations"
+  | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs)));
 
 fun pretty_dependencies ctxt clean export insts =
   let
diff -r f4fb93197670 -r 70f9826753f6 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Sep 24 19:43:20 2018 +0200
+++ b/src/Pure/Pure.thy	Mon Sep 24 19:53:45 2018 +0200
@@ -1097,8 +1097,10 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_locales\<close>
     "print locales of this theory"
-    (Parse.opt_bang >> (fn b =>
-      Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
+    (Parse.opt_bang >> (fn verbose =>
+      Toplevel.keep (fn state =>
+        let val thy = Toplevel.theory_of state
+        in Pretty.writeln (Locale.pretty_locales thy verbose) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_classes\<close>
@@ -1118,8 +1120,13 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_interps\<close>
     "print interpretations of locale for this theory or proof context"
-    (Parse.position Parse.name >> (fn name =>
-      Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
+    (Parse.position Parse.name >> (fn raw_name =>
+      Toplevel.keep (fn state =>
+        let
+          val ctxt = Toplevel.context_of state;
+          val thy = Toplevel.theory_of state;
+          val name = Locale.check thy raw_name;
+        in Pretty.writeln (Locale.pretty_registrations ctxt name) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_dependencies\<close>