equal
deleted
inserted
replaced
109 |
109 |
110 type browser_info = |
110 type browser_info = |
111 {theories: theory_info Symtab.table, |
111 {theories: theory_info Symtab.table, |
112 tex_index: (int * string) list, |
112 tex_index: (int * string) list, |
113 html_index: (int * string) list, |
113 html_index: (int * string) list, |
114 graph: Graph_Display.graph}; |
114 graph: Graph_Display.entry list}; |
115 |
115 |
116 fun make_browser_info (theories, tex_index, html_index, graph) : browser_info = |
116 fun make_browser_info (theories, tex_index, html_index, graph) : browser_info = |
117 {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph}; |
117 {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph}; |
118 |
118 |
119 val empty_browser_info = make_browser_info (Symtab.empty, [], [], []); |
119 val empty_browser_info = make_browser_info (Symtab.empty, [], [], []); |