stan/jdk-24
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

8227416: Add a "Table Of Contents" to HTML version of man pages

Browse Source 
Reviewed-by: mchung
This commit is contained in:
Jonathan Gibbons 2019-07-10 16:23:59 -07:00
parent cf39d96d3a
commit 2cbbe809a6
3 changed files with 30 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
make/Docs.gmk
View File

@ -626,7 +626,7 @@ ifeq ($(ENABLE_PANDOC), true)
FILTER := $(PANDOC_HTML_MANPAGE_FILTER), \
CSS := $(GLOBAL_SPECS_DEFAULT_CSS_FILE), \
REPLACEMENTS := @@VERSION_SHORT@@ => $(VERSION_SHORT), \
OPTIONS := -V include-before='$(SPECS_TOP)' -V include-after='$(SPECS_BOTTOM_1)', \
OPTIONS := --toc -V include-before='$(SPECS_TOP)' -V include-after='$(SPECS_BOTTOM_1)', \
POST_PROCESS := $(TOOL_FIXUPPANDOC), \
EXTRA_DEPS := $(PANDOC_HTML_MANPAGE_FILTER) \
$(PANDOC_HTML_MANPAGE_FILTER_JAVASCRIPT), \

21
make/data/docs-resources/resources/jdk-default.css
View File

@ -1,5 +1,5 @@
/*
* Copyright (c) 2017, 2018, Oracle and/or its affiliates. All rights reserved.
* Copyright (c) 2017, 2019, Oracle and/or its affiliates. All rights reserved.
* DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
*
* This code is free software; you can redistribute it and/or modify it
@ -162,3 +162,22 @@ table.centered td {
font-style: italic;
font-size: 80%;
}
nav#TOC {
border: 1px solid gray;
border-radius: 10px;
padding: 5px 10px;
margin-bottom: 15px;
}
nav#TOC ul ul {
font-size:smaller;
}
nav#TOC ul ul li {
display: inline-block
}
nav#TOC ul ul li::before {
content: " \2022 "
}

9
make/jdk/src/classes/build/tools/fixuppandoc/Main.java
View File

@ -81,6 +81,10 @@ import java.util.regex.Pattern;
*
* Update the content string, to indicate it has been processed by this program.
*
* <h2>{@code <nav id="TOC">}</h2>
*
* Set attribute {@code title="Table Of Contents"}
*
*/
public class Main {
/**
@ -273,6 +277,11 @@ public class Main {
}
// <main> is not permitted within these elements
allowMain = false;
if (name.equals("nav") && Objects.equals(attrs.get("id"), "TOC")) {
out.write(buffer.toString()
.replaceAll(">$", " title=\"Table Of Contents\">"));
buffer.setLength(0);
}
break;
case "body":