session graph with folded base theories, as in document preparation;
authorwenzelm
Wed Apr 15 19:08:37 2015 +0200 (2015-04-15 ago)
changeset 60082d3573eb7728f
parent 60081 9fb7b44e3e7e
child 60083 6d6d652ee029
session graph with folded base theories, as in document preparation;
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 15 17:34:45 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 15 19:08:37 2015 +0200
     1.3 @@ -270,33 +270,22 @@
     1.4  
     1.5  (* display dependencies *)
     1.6  
     1.7 -val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
     1.8 -  let
     1.9 -    val thy = Toplevel.theory_of state;
    1.10 -    val thy_session = Present.session_name thy;
    1.11 -  in
    1.12 -    Theory.nodes_of thy
    1.13 -    |> map (fn thy_node =>
    1.14 -        let
    1.15 -          val name = Context.theory_name thy_node;
    1.16 -          val parents = map Context.theory_name (Theory.parents_of thy_node);
    1.17 -          val session = Present.session_name thy_node;
    1.18 -          val node =
    1.19 -            Graph_Display.session_node
    1.20 -              {name = name, directory = session, unfold = session = thy_session, path = ""};
    1.21 -        in ((name, node), parents) end)
    1.22 -    |> Graph_Display.display_graph
    1.23 -  end);
    1.24 +val thy_deps =
    1.25 +  Toplevel.unknown_theory o
    1.26 +  Toplevel.keep (fn st =>
    1.27 +    let
    1.28 +      val thy = Toplevel.theory_of st;
    1.29 +      val parent_session = Session.get_name ();
    1.30 +      val parent_loaded = is_some o Thy_Info.lookup_theory;
    1.31 +    in Graph_Display.display_graph (Present.session_graph parent_session parent_loaded thy) end);
    1.32  
    1.33 -val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.34 -  let
    1.35 -    val thy = Toplevel.theory_of state;
    1.36 -  in
    1.37 +val locale_deps =
    1.38 +  Toplevel.unknown_theory o
    1.39 +  Toplevel.keep (Toplevel.theory_of #> (fn thy =>
    1.40      Locale.pretty_locale_deps thy
    1.41      |> map (fn {name, parents, body} =>
    1.42        ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
    1.43 -    |> Graph_Display.display_graph
    1.44 -  end);
    1.45 +    |> Graph_Display.display_graph));
    1.46  
    1.47  
    1.48  (* print theorems, terms, types etc. *)
     2.1 --- a/src/Pure/Thy/present.ML	Wed Apr 15 17:34:45 2015 +0200
     2.2 +++ b/src/Pure/Thy/present.ML	Wed Apr 15 19:08:37 2015 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  signature PRESENT =
     2.5  sig
     2.6    val session_name: theory -> string
     2.7 +  val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list
     2.8    val document_enabled: string -> bool
     2.9    val document_variants: string -> (string * string) list
    2.10    val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
    2.11 @@ -54,6 +55,28 @@
    2.12  val session_name = #name o Browser_Info.get;
    2.13  
    2.14  
    2.15 +(* session graph *)
    2.16 +
    2.17 +fun session_graph parent_session parent_loaded =
    2.18 +  let
    2.19 +    val parent_session_name = "session." ^ parent_session;
    2.20 +    val parent_session_node = Graph_Display.content_node ("[" ^ parent_session ^ "]") [];
    2.21 +    fun node_name name = if parent_loaded name then parent_session_name else "theory." ^ name;
    2.22 +    fun theory_entry thy =
    2.23 +      let
    2.24 +        val name = Context.theory_name thy;
    2.25 +        val deps = map (node_name o Context.theory_name) (Theory.parents_of thy);
    2.26 +      in
    2.27 +        if parent_loaded name then NONE
    2.28 +        else SOME ((node_name name, Graph_Display.content_node name []), deps)
    2.29 +      end;
    2.30 +  in
    2.31 +    fn thy =>
    2.32 +      ((parent_session_name, parent_session_node), []) ::
    2.33 +        map_filter theory_entry (Theory.nodes_of thy)
    2.34 +  end;
    2.35 +
    2.36 +
    2.37  
    2.38  (** global browser info state **)
    2.39  
    2.40 @@ -366,4 +389,3 @@
    2.41    end);
    2.42  
    2.43  end;
    2.44 -