# HG changeset patch
# User ballarin
# Date 1574752184 -3600
# Node ID c9433e8e314efaafa7d48b1d741b7a522c37a102
# Parent  03afc82522255778a5f4506307c3413319988986
Remove diagnostic command 'print_dependencies'.

diff -r 03afc8252225 -r c9433e8e314e NEWS
--- a/NEWS	Mon Nov 25 13:28:31 2019 +0100
+++ b/NEWS	Tue Nov 26 08:09:44 2019 +0100
@@ -43,7 +43,8 @@
 and may thus improve scalability.
 
 * New attribute "trace_locales" for tracing activation of locale
-instances during roundup.
+instances during roundup.  It replaces the diagnostic command
+'print_dependencies', which was removed.
 
 
 *** Isabelle/jEdit Prover IDE ***
diff -r 03afc8252225 -r c9433e8e314e src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Nov 25 13:28:31 2019 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Tue Nov 26 08:09:44 2019 +0100
@@ -618,7 +618,6 @@
 
   \<^descr> \<^theory_text>\<open>locale_deps\<close> visualizes all locales and their relations as a Hasse
   diagram. This includes locales defined as type classes (\secref{sec:class}).
-  See also \<^theory_text>\<open>print_dependencies\<close> below.
 
   \<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all
   introduction rules of locale predicates of the theory. While @{method
@@ -644,7 +643,6 @@
     @{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
     @{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
     @{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
-    @{command_def "print_dependencies"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{command_def "print_interps"}\<open>\<^sup>*\<close> & :  & \<open>context \<rightarrow>\<close> \\
   \end{matharray}
 
@@ -665,8 +663,6 @@
     @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
       definitions?
     ;
-    @@{command print_dependencies} '!'? @{syntax locale_expr}
-    ;
     @@{command print_interps} @{syntax name}
     ;
 
@@ -760,15 +756,7 @@
   locale argument must be omitted. The command then refers to the locale (or
   class) target of the context block.
 
-  \<^descr> \<^theory_text>\<open>print_dependencies expr\<close> is useful for understanding the effect of an
-  interpretation of \<open>expr\<close> in the current context. It lists all locale
-  instances for which interpretations would be added to the current context.
-  Variant \<^theory_text>\<open>print_dependencies!\<close> 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.
-
-  \<^descr> \<^theory_text>\<open>print_interps locale\<close> lists all interpretations of \<open>locale\<close> in the
+  \<^descr> \<^theory_text>\<open>print_interps name\<close> lists all interpretations of locale \<open>name\<close> in the
   current theory or proof context, including those due to a combination of an
   \<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close>
   declarations.
diff -r 03afc8252225 -r c9433e8e314e src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Nov 25 13:28:31 2019 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Tue Nov 26 08:09:44 2019 +0100
@@ -814,7 +814,6 @@
     then interpret local_fixed: lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close>
       by unfold_locales
     thm local_fixed.lone
-    print_dependencies! lgrp \<open>(+)\<close> \<open>0\<close> \<open>minus\<close> + lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close>
   }
   assume \<open>!!x zero. zero + x = x\<close> \<open>!!x zero. (-x) + x = zero\<close>
   then interpret local_free: lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close> for zero
diff -r 03afc8252225 -r c9433e8e314e src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Nov 25 13:28:31 2019 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Nov 26 08:09:44 2019 +0100
@@ -42,9 +42,6 @@
     (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
   val read_goal_expression: expression -> Proof.context ->
     (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
-
-  (* Diagnostic *)
-  val pretty_dependencies: Proof.context -> bool -> expression -> Pretty.T
 end;
 
 structure Expression : EXPRESSION =
@@ -872,15 +869,4 @@
 
 end;
 
-
-(** Print the instances that would be activated by an interpretation
-  of the expression in the current context (clean = false) or in an
-  empty context (clean = true). **)
-
-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.pretty_dependencies expr_ctxt clean export' deps end;
-
 end;
diff -r 03afc8252225 -r c9433e8e314e src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Nov 25 13:28:31 2019 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Nov 26 08:09:44 2019 +0100
@@ -90,7 +90,6 @@
   val pretty_locales: theory -> bool -> Pretty.T
   val pretty_locale: theory -> bool -> string -> Pretty.T
   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
   type locale_dependency =
     {source: string, target: string, prefix: (string * bool) list, morphism: morphism,
@@ -760,16 +759,6 @@
     [] => 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
-    val thy = Proof_Context.theory_of ctxt;
-    val idents = if clean then empty_idents else Idents.get (Context.Proof ctxt);
-  in
-    (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;
-
 fun pretty_locale_deps thy =
   let
     fun make_node name =
diff -r 03afc8252225 -r c9433e8e314e src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Nov 25 13:28:31 2019 +0100
+++ b/src/Pure/Pure.thy	Tue Nov 26 08:09:44 2019 +0100
@@ -81,7 +81,7 @@
   and "help" "print_commands" "print_options" "print_context" "print_theory"
     "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules"
     "print_theorems" "print_locales" "print_classes" "print_locale"
-    "print_interps" "print_dependencies" "print_attributes"
+    "print_interps" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     "print_antiquotations" "print_ML_antiquotations" "thy_deps"
     "locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings"
@@ -1165,13 +1165,6 @@
         in Pretty.writeln (Locale.pretty_registrations ctxt name) end)));
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>print_dependencies\<close>
-    "print dependencies of locale expression"
-    (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>
     "print attributes of this theory"
     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));