# 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 = "" ^ txt ^ "";
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 ^ "
\n" ^
- HTML.keyword symbols "imports" ^ " " ^
- space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^
- "
\n\n\n
" :: + (if null Bs then "" + else + HTML.keyword symbols "imports" ^ " " ^ + space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "
\n") ^ + "\n
" :: body @ ["\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;