# HG changeset patch
# User wenzelm
# Date 1215526763 -7200
# Node ID ac1d6e87aa52b9fd53571b610cf90f8a53b02ce1
# Parent  16570181ca4432d0382b6415088644f31af8c7a4
removed unused href_opt_name;
begin_theory: unconditional file links, proper output of parentheses;

diff -r 16570181ca44 -r ac1d6e87aa52 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Jul 08 13:45:27 2008 +0200
+++ b/src/Pure/Thy/html.ML	Tue Jul 08 16:19:23 2008 +0200
@@ -17,7 +17,6 @@
   val file_path: Url.T -> text
   val href_name: string -> text -> text
   val href_path: Url.T -> text -> text
-  val href_opt_name: string option -> text -> text
   val href_opt_path: Url.T option -> text -> text
   val para: text -> text
   val preform: text -> text
@@ -32,7 +31,7 @@
   val session_entries: (Url.T * string) list -> text
   val verbatim_source: Symbol.symbol list -> text
   val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
-    (Url.T option * Url.T * bool) list -> text -> text
+    (Url.T * Url.T * bool) list -> text -> text
   val end_theory: text
   val ml_file: Url.T -> string -> text
   val results: Proof.context -> string -> (string * thm list) list -> text
@@ -267,9 +266,6 @@
 fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
 fun href_path path txt = href_name (Url.implode path) txt;
 
-fun href_opt_name NONE txt = txt
-  | href_opt_name (SOME s) txt = href_name s txt;
-
 fun href_opt_path NONE txt = txt
   | href_opt_path (SOME p) txt = href_path p txt;
 
@@ -362,8 +358,8 @@
 
 
 local
-  fun file (opt_ref, path, loadit) =
-    href_opt_path opt_ref (if loadit then enclose "(" ")" (file_path path) else file_path path);
+  fun file (href, path, loadit) =
+    href_path href (if loadit then file_path path else enclose "(" ")" (file_path path));
 
   fun theory up A =
     begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^