# HG changeset patch
# User wenzelm
# Date 1605628489 -3600
# Node ID 09ee9eb7a3d31d8931de3232a416a16cb8ac8f15
# Parent  2a329baa7d397b6cb8cc0a8f7ab456b1181dd736
proper link for Pure;

diff -r 2a329baa7d39 -r 09ee9eb7a3d3 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Nov 17 16:48:18 2020 +0100
+++ b/src/Pure/Thy/html.ML	Tue Nov 17 16:54:49 2020 +0100
@@ -16,7 +16,6 @@
   val command: symbols -> string -> text
   val href_name: string -> string -> string
   val href_path: Url.T -> string -> string
-  val href_opt_path: Url.T option -> string -> string
   val begin_document: symbols -> string -> text
   val end_document: text
 end;
@@ -120,9 +119,6 @@
 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
 fun href_path path txt = href_name (Url.implode path) txt;
 
-fun href_opt_path NONE txt = txt
-  | href_opt_path (SOME p) txt = href_path p txt;
-
 
 (* document *)
 
diff -r 2a329baa7d39 -r 09ee9eb7a3d3 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Nov 17 16:48:18 2020 +0100
+++ b/src/Pure/Thy/present.ML	Tue Nov 17 16:54:49 2020 +0100
@@ -41,18 +41,19 @@
     val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy');
     val link = html_name thy';
   in
-    if session = session' then SOME link
-    else if chapter = chapter' then SOME (Path.parent + Path.basic session' + link)
-    else if chapter' = Context.PureN then NONE
-    else SOME (Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link)
+    if session = session' then link
+    else if chapter = chapter' then Path.parent + Path.basic session' + link
+    else Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link
   end;
 
 fun theory_document symbols A Bs body =
   HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^
   HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^
-  HTML.keyword symbols "imports" ^ " " ^
-    space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^
-  "<br/>\n\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
+  (if null Bs then ""
+   else
+    HTML.keyword symbols "imports" ^ " " ^
+      space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "<br/>\n") ^
+  "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
   body @ ["</pre>\n", HTML.end_document];
 
 in
@@ -62,7 +63,7 @@
     val name = Context.theory_name thy;
     val parents =
       Theory.parents_of thy |> map (fn thy' =>
-        (Option.map Url.File (theory_link thy thy'), Context.theory_name thy'));
+        (Url.File (theory_link thy thy'), Context.theory_name thy'));
 
     val symbols = Resources.html_symbols ();
     val keywords = Thy_Header.get_keywords thy;