equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature PRESENT = |
7 signature PRESENT = |
8 sig |
8 sig |
9 val session_name: theory -> string |
9 val session_name: theory -> string |
10 val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list |
|
11 val document_enabled: string -> bool |
10 val document_enabled: string -> bool |
12 val document_variants: string -> (string * string) list |
11 val document_variants: string -> (string * string) list |
13 val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> |
12 val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> |
14 (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit |
13 (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit |
15 val finish: unit -> unit |
14 val finish: unit -> unit |
51 |
50 |
52 val _ = Theory.setup |
51 val _ = Theory.setup |
53 (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}); |
52 (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}); |
54 |
53 |
55 val session_name = #name o Browser_Info.get; |
54 val session_name = #name o Browser_Info.get; |
56 |
|
57 |
|
58 (* session graph *) |
|
59 |
|
60 fun session_graph parent_session parent_loaded = |
|
61 let |
|
62 val parent_session_name = "session." ^ parent_session; |
|
63 val parent_session_node = Graph_Display.content_node ("[" ^ parent_session ^ "]") []; |
|
64 fun node_name name = if parent_loaded name then parent_session_name else "theory." ^ name; |
|
65 fun theory_entry thy = |
|
66 let |
|
67 val name = Context.theory_name thy; |
|
68 val deps = map (node_name o Context.theory_name) (Theory.parents_of thy); |
|
69 in |
|
70 if parent_loaded (Context.theory_long_name thy) then NONE |
|
71 else SOME ((node_name name, Graph_Display.content_node name []), deps) |
|
72 end; |
|
73 in |
|
74 fn thy => |
|
75 ((parent_session_name, parent_session_node), []) :: |
|
76 map_filter theory_entry (Theory.nodes_of thy) |
|
77 end; |
|
78 |
55 |
79 |
56 |
80 |
57 |
81 (** global browser info state **) |
58 (** global browser info state **) |
82 |
59 |