# HG changeset patch # User wenzelm # Date 1300648841 -3600 # Node ID 04f8c485121905015b3fbddfd22e3f8d5b921b33 # Parent b008525c43995e42b1439683df908751b5523d8b eliminated dead code; diff -r b008525c4399 -r 04f8c4851219 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Mar 20 20:05:43 2011 +0100 +++ b/src/Pure/Thy/present.ML Sun Mar 20 20:20:41 2011 +0100 @@ -108,7 +108,6 @@ let val name = Context.theory_name thy; val {name = sess_name, session, is_local} = get_info thy; - val path' = Path.append (Path.make session) (html_path name); val entry = {name = name, ID = ID_of session name, dir = sess_name, path = @@ -173,7 +172,7 @@ (Symtab.update (name, info) theories, files, tex_index, html_index, graph)); fun change_theory_info name f = - change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) => + change_browser_info (fn (theories, files, tex_index, html_index, graph) => (case Symtab.lookup theories name of NONE => error ("Browser info: cannot access theory document " ^ quote name) | SOME info => (Symtab.update (name, map_theory_info f info) theories, files, @@ -204,9 +203,6 @@ fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) => (tex_source, Buffer.add txt html_source, html)); -fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) => - (tex_source, html_source, Buffer.add txt html)); - (** global session state **)