Improvements to the print_dependencies command.
authorballarin
Wed Mar 27 22:36:03 2013 +0100 (2013-03-27)
changeset 515655e9fdbdf88ce
parent 51564 bfdc3f720bd6
child 51566 8e97017538ba
child 51571 1eb3316d6d93
Improvements to the print_dependencies command.
NEWS
src/Doc/IsarRef/Spec.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/NEWS	Wed Mar 27 21:25:33 2013 +0100
     1.2 +++ b/NEWS	Wed Mar 27 22:36:03 2013 +0100
     1.3 @@ -31,6 +31,8 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Improved locales diagnostic command 'print_dependencies'.
     1.8 +
     1.9  * Discontinued obsolete 'axioms' command, which has been marked as
    1.10  legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
    1.11  instead, while observing its uniform scope for polymorphism.
     2.1 --- a/src/Doc/IsarRef/Spec.thy	Wed Mar 27 21:25:33 2013 +0100
     2.2 +++ b/src/Doc/IsarRef/Spec.thy	Wed Mar 27 22:36:03 2013 +0100
     2.3 @@ -701,13 +701,14 @@
     2.4    understanding the effect of an interpretation of @{text "expr"}.  It
     2.5    lists all locale instances for which interpretations would be added
     2.6    to the current context.  Variant @{command
     2.7 -  "print_dependencies"}@{text "!"} prints all locale instances that
     2.8 -  would be considered for interpretation, and would be interpreted in
     2.9 -  an empty context (that is, without interpretations).
    2.10 +  "print_dependencies"}@{text "!"} does not generalize parameters and
    2.11 +  assumes an empty context --- that is, it prints all locale instances
    2.12 +  that would be considered for interpretation.  The latter is useful
    2.13 +  for understanding the dependencies of a locale expression.
    2.14  
    2.15    \item @{command "print_interps"}~@{text "locale"} lists all
    2.16    interpretations of @{text "locale"} in the current theory or proof
    2.17 -  context, including those due to a combination of a @{command
    2.18 +  context, including those due to a combination of an @{command
    2.19    "interpretation"} or @{command "interpret"} and one or several
    2.20    @{command "sublocale"} declarations.
    2.21  
     3.1 --- a/src/Pure/Isar/expression.ML	Wed Mar 27 21:25:33 2013 +0100
     3.2 +++ b/src/Pure/Isar/expression.ML	Wed Mar 27 22:36:03 2013 +0100
     3.3 @@ -938,9 +938,9 @@
     3.4  fun print_dependencies ctxt clean expression =
     3.5    let
     3.6      val ((_, deps, export), expr_ctxt) = read_goal_expression expression ctxt;
     3.7 +    val export' = if clean then Morphism.identity else export;
     3.8    in
     3.9 -    Locale.print_dependencies expr_ctxt clean export deps
    3.10 +    Locale.print_dependencies expr_ctxt clean export' deps
    3.11    end;
    3.12  
    3.13  end;
    3.14 -
     4.1 --- a/src/Pure/Isar/locale.ML	Wed Mar 27 21:25:33 2013 +0100
     4.2 +++ b/src/Pure/Isar/locale.ML	Wed Mar 27 22:36:03 2013 +0100
     4.3 @@ -209,10 +209,11 @@
     4.4  
     4.5  (* Print instance and qualifiers *)
     4.6  
     4.7 -fun pretty_reg ctxt (name, morph) =
     4.8 +fun pretty_reg ctxt export (name, morph) =
     4.9    let
    4.10      val thy = Proof_Context.theory_of ctxt;
    4.11      val name' = extern thy name;
    4.12 +    val morph' = morph $> export;
    4.13      fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
    4.14      fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
    4.15      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    4.16 @@ -224,8 +225,8 @@
    4.17      fun prt_inst ts =
    4.18        Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
    4.19  
    4.20 -    val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
    4.21 -    val ts = instance_of thy name morph;
    4.22 +    val qs = Binding.name "x" |> Morphism.binding morph' |> Binding.prefix_of;
    4.23 +    val ts = instance_of thy name morph';
    4.24    in
    4.25      (case qs of
    4.26        [] => prt_inst ts
    4.27 @@ -638,7 +639,7 @@
    4.28    in
    4.29      (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
    4.30        [] => Pretty.str "no interpretations"
    4.31 -    | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
    4.32 +    | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs)))
    4.33    end |> Pretty.writeln;
    4.34  
    4.35  fun print_dependencies ctxt clean export insts =
    4.36 @@ -648,7 +649,7 @@
    4.37    in
    4.38      (case fold (roundup thy cons export) insts (idents, []) |> snd of
    4.39        [] => Pretty.str "no dependencies"
    4.40 -    | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
    4.41 +    | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt export) (rev deps)))
    4.42    end |> Pretty.writeln;
    4.43  
    4.44  fun pretty_locale_deps thy =