proper link location;
authorwenzelm
Tue, 17 Nov 2020 16:48:18 +0100
changeset 72871 2a329baa7d39
parent 72870 5cea0993ee4f
child 72872 09ee9eb7a3d3
proper link location;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Nov 17 16:34:01 2020 +0100
+++ b/src/Pure/Thy/present.ML	Tue Nov 17 16:48:18 2020 +0100
@@ -42,9 +42,9 @@
     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)
+    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)
   end;
 
 fun theory_document symbols A Bs body =