src/Pure/Isar/expression.ML
changeset 41435 12585dfb86fe
parent 41270 dea60d052923
child 41585 45d7da4e4ccf
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Jan 06 21:06:17 2011 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Jan 06 21:06:18 2011 +0100
     1.3 @@ -51,6 +51,9 @@
     1.4      bool -> Proof.state -> Proof.state
     1.5    val interpret_cmd: expression -> (Attrib.binding * string) list ->
     1.6      bool -> Proof.state -> Proof.state
     1.7 +
     1.8 +  (* Diagnostic *)
     1.9 +  val print_dependencies: Proof.context -> bool -> expression -> unit
    1.10  end;
    1.11  
    1.12  structure Expression : EXPRESSION =
    1.13 @@ -913,12 +916,6 @@
    1.14        note_eqns_dependency target deps witss attrss eqns export export';
    1.15  
    1.16    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.17 -(*
    1.18 -    fun after_qed witss = ProofContext.background_theory
    1.19 -      (fold (fn ((dep, morph), wits) => Locale.add_dependency
    1.20 -        target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
    1.21 -  in Element.witness_proof after_qed propss goal_ctxt end;
    1.22 -*)
    1.23  in
    1.24  
    1.25  fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    1.26 @@ -927,5 +924,17 @@
    1.27  
    1.28  end;
    1.29  
    1.30 +
    1.31 +(** Print the instances that would be activated by an interpretation
    1.32 +  of the expression in the current context (clean = false) or in an
    1.33 +  empty context (clean = true). **)
    1.34 +
    1.35 +fun print_dependencies ctxt clean expression =
    1.36 +  let
    1.37 +    val ((_, deps, export), expr_ctxt) = read_goal_expression expression ctxt;
    1.38 +  in
    1.39 +    Locale.print_dependencies expr_ctxt clean export deps
    1.40 +  end;
    1.41 +
    1.42  end;
    1.43