src/Pure/Isar/isar_cmd.ML
changeset 37866 cd1d1bc7684c
parent 37305 9763792e4ac7
child 37870 dd9cfc512b7f
equal deleted inserted replaced
37865:3a6ec95a9f68 37866:cd1d1bc7684c
   406 val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations;
   406 val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations;
   407 
   407 
   408 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   408 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   409   let
   409   let
   410     val thy = Toplevel.theory_of state;
   410     val thy = Toplevel.theory_of state;
       
   411     val thy_session = Present.session_name thy;
       
   412 
   411     val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
   413     val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
   412     val gr = all_thys |> map (fn node =>
   414     val gr = all_thys |> map (fn node =>
   413       let
   415       let
   414         val name = Context.theory_name node;
   416         val name = Context.theory_name node;
   415         val parents = map Context.theory_name (Theory.parents_of node);
   417         val parents = map Context.theory_name (Theory.parents_of node);
   416         val dir = Present.session_name node;
   418         val session = Present.session_name node;
   417         val unfold = not (Thy_Info.known_thy name andalso Thy_Info.is_finished name);
   419         val unfold = (session = thy_session);
   418       in {name = name, ID = name, parents = parents, dir = dir, unfold = unfold, path = ""} end);
   420       in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end);
   419   in Present.display_graph gr end);
   421   in Present.display_graph gr end);
   420 
   422 
   421 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   423 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   422   let
   424   let
   423     val thy = Toplevel.theory_of state;
   425     val thy = Toplevel.theory_of state;