# HG changeset patch
# User ballarin
# Date 1364420163 -3600
# Node ID 5e9fdbdf88ce145f831ad9eea13441bcb91f0065
# Parent  bfdc3f720bd64aed9258336cc90aca0beedee2a7
Improvements to the print_dependencies command.

diff -r bfdc3f720bd6 -r 5e9fdbdf88ce NEWS
--- a/NEWS	Wed Mar 27 21:25:33 2013 +0100
+++ b/NEWS	Wed Mar 27 22:36:03 2013 +0100
@@ -31,6 +31,8 @@
 
 *** Pure ***
 
+* Improved locales diagnostic command 'print_dependencies'.
+
 * Discontinued obsolete 'axioms' command, which has been marked as
 legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
 instead, while observing its uniform scope for polymorphism.
diff -r bfdc3f720bd6 -r 5e9fdbdf88ce src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Wed Mar 27 21:25:33 2013 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Wed Mar 27 22:36:03 2013 +0100
@@ -701,13 +701,14 @@
   understanding the effect of an interpretation of @{text "expr"}.  It
   lists all locale instances for which interpretations would be added
   to the current context.  Variant @{command
-  "print_dependencies"}@{text "!"} prints all locale instances that
-  would be considered for interpretation, and would be interpreted in
-  an empty context (that is, without interpretations).
+  "print_dependencies"}@{text "!"} does not generalize parameters and
+  assumes an empty context --- that is, it prints all locale instances
+  that would be considered for interpretation.  The latter is useful
+  for understanding the dependencies of a locale expression.
 
   \item @{command "print_interps"}~@{text "locale"} lists all
   interpretations of @{text "locale"} in the current theory or proof
-  context, including those due to a combination of a @{command
+  context, including those due to a combination of an @{command
   "interpretation"} or @{command "interpret"} and one or several
   @{command "sublocale"} declarations.
 
diff -r bfdc3f720bd6 -r 5e9fdbdf88ce src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Mar 27 21:25:33 2013 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Mar 27 22:36:03 2013 +0100
@@ -938,9 +938,9 @@
 fun print_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
+    Locale.print_dependencies expr_ctxt clean export' deps
   end;
 
 end;
-
diff -r bfdc3f720bd6 -r 5e9fdbdf88ce src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Mar 27 21:25:33 2013 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Mar 27 22:36:03 2013 +0100
@@ -209,10 +209,11 @@
 
 (* Print instance and qualifiers *)
 
-fun pretty_reg ctxt (name, morph) =
+fun pretty_reg ctxt export (name, morph) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val name' = extern thy name;
+    val morph' = morph $> export;
     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
@@ -224,8 +225,8 @@
     fun prt_inst ts =
       Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
 
-    val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
-    val ts = instance_of thy name morph;
+    val qs = Binding.name "x" |> Morphism.binding morph' |> Binding.prefix_of;
+    val ts = instance_of thy name morph';
   in
     (case qs of
       [] => prt_inst ts
@@ -638,7 +639,7 @@
   in
     (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
       [] => Pretty.str "no interpretations"
-    | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
+    | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs)))
   end |> Pretty.writeln;
 
 fun print_dependencies ctxt clean export insts =
@@ -648,7 +649,7 @@
   in
     (case fold (roundup thy cons export) insts (idents, []) |> snd of
       [] => Pretty.str "no dependencies"
-    | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
+    | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt export) (rev deps)))
   end |> Pretty.writeln;
 
 fun pretty_locale_deps thy =