tuned;
authorwenzelm
Thu Apr 16 16:19:39 2015 +0200 (2015-04-16 ago)
changeset 601003c66b0a9d7b0
parent 60099 d20ca79d50e4
child 60101 73c260342704
tuned;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 15:22:44 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 16:19:39 2015 +0200
     1.3 @@ -35,7 +35,6 @@
     1.4    val diag_state: Proof.context -> Toplevel.state
     1.5    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
     1.6    val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
     1.7 -  val locale_deps: Toplevel.transition -> Toplevel.transition
     1.8    val print_stmts: string list * (Facts.ref * Token.src list) list
     1.9      -> Toplevel.transition -> Toplevel.transition
    1.10    val print_thms: string list * (Facts.ref * Token.src list) list
    1.11 @@ -264,16 +263,6 @@
    1.12      in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
    1.13  
    1.14  
    1.15 -(* display dependencies *)
    1.16 -
    1.17 -val locale_deps =
    1.18 -  Toplevel.keep (Toplevel.theory_of #> (fn thy =>
    1.19 -    Locale.pretty_locale_deps thy
    1.20 -    |> map (fn {name, parents, body} =>
    1.21 -      ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
    1.22 -    |> Graph_Display.display_graph));
    1.23 -
    1.24 -
    1.25  (* print theorems, terms, types etc. *)
    1.26  
    1.27  local
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 16 15:22:44 2015 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 16 16:19:39 2015 +0200
     2.3 @@ -789,7 +789,12 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
     2.7 -    (Scan.succeed Isar_Cmd.locale_deps);
     2.8 +    (Scan.succeed
     2.9 +      (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
    2.10 +        Locale.pretty_locale_deps thy
    2.11 +        |> map (fn {name, parents, body} =>
    2.12 +          ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
    2.13 +        |> Graph_Display.display_graph))));
    2.14  
    2.15  val _ =
    2.16    Outer_Syntax.command @{command_keyword print_term_bindings}