thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
authorwenzelm
Sat Sep 08 19:58:36 2007 +0200 (2007-09-08)
changeset 245602693220bd77f
parent 24559 dae0972c0066
child 24561 7b4aa14d2491
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Sep 08 19:58:35 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Sep 08 19:58:36 2007 +0200
     1.3 @@ -486,12 +486,14 @@
     1.4  val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
     1.5    let
     1.6      val thy = Toplevel.theory_of state;
     1.7 -    val all_thys = sort Context.thy_ord (thy :: Theory.ancestors_of thy);
     1.8 +    val all_thys = sort ThyInfo.thy_ord (thy :: Theory.ancestors_of thy);
     1.9      val gr = all_thys |> map (fn node =>
    1.10        let
    1.11          val name = Context.theory_name node;
    1.12          val parents = map Context.theory_name (Theory.parents_of node);
    1.13 -      in {name = name, ID = name, parents = parents, dir = "", unfold = true, path = ""} end);
    1.14 +        val dir = Present.session_name node;
    1.15 +        val unfold = not (ThyInfo.known_thy name andalso ThyInfo.is_finished name);
    1.16 +      in {name = name, ID = name, parents = parents, dir = dir, unfold = unfold, path = ""} end);
    1.17    in Present.display_graph gr end);
    1.18  
    1.19  val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.20 @@ -513,7 +515,7 @@
    1.21  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.22    ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
    1.23  
    1.24 -fun find_theorems ((opt_lim, rem_dups), spec) = 
    1.25 +fun find_theorems ((opt_lim, rem_dups), spec) =
    1.26    Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.27    let
    1.28      val proof_state = Toplevel.enter_proof_body state;