1- window . addEventListener ( "DOMContentLoaded" , ( ) => {
1+ let observer = null ;
22
3- var toggler = document . getElementById ( "leftToggler" ) ;
4- if ( toggler ) {
5- toggler . onclick = function ( ) {
6- document . getElementById ( "leftColumn" ) . classList . toggle ( "open" ) ;
7- } ;
3+ function attachAllListeners ( ) {
4+ if ( observer ) {
5+ observer . disconnect ( )
86 }
97
108 var scrollPosition = sessionStorage . getItem ( "scroll_value" ) ;
@@ -60,19 +58,53 @@ window.addEventListener("DOMContentLoaded", () => {
6058 $ ( this ) . parent ( ) . toggleClass ( "expanded" ) ;
6159 } ) ;
6260
61+ document . querySelectorAll ( 'a' ) . forEach ( el => {
62+ const href = el . href
63+ if ( href === "" ) { return }
64+ const url = new URL ( href )
65+ el . addEventListener ( 'click' , e => {
66+ if ( url . href . replace ( "#" , "" ) === window . location . href . replace ( "#" , "" ) ) { return }
67+ if ( url . origin !== window . location . origin ) { return }
68+ if ( e . metaKey || e . ctrlKey || e . shiftKey || e . altKey || e . button !== 0 ) { return }
69+ e . preventDefault ( )
70+ e . stopPropagation ( )
71+ $ . get ( href , function ( data ) {
72+ const html = $ . parseHTML ( data )
73+ const title = html . find ( node => node . nodeName === "TITLE" ) . innerText
74+ const bodyDiv = html . find ( node => node . nodeName === "DIV" )
75+ const { children } = document . body . firstChild
76+ if ( window . history . state === null ) {
77+ window . history . replaceState ( {
78+ leftColumn : children [ 3 ] . innerHTML ,
79+ mainDiv : children [ 6 ] . innerHTML ,
80+ title : document . title ,
81+ } , '' )
82+ }
83+ document . title = title
84+ const leftColumn = bodyDiv . children [ 3 ] . innerHTML
85+ const mainDiv = bodyDiv . children [ 6 ] . innerHTML
86+ window . history . pushState ( { leftColumn, mainDiv, title } , '' , href )
87+ children [ 3 ] . innerHTML = leftColumn
88+ children [ 6 ] . innerHTML = mainDiv
89+ attachAllListeners ( )
90+ } )
91+ } )
92+ } )
93+
6394 $ ( ".ar" ) . on ( "click" , function ( e ) {
6495 $ ( this ) . parent ( ) . parent ( ) . toggleClass ( "expanded" ) ;
6596 $ ( this ) . toggleClass ( "expanded" ) ;
6697 e . stopPropagation ( ) ;
6798 } ) ;
6899
69- document . querySelectorAll ( ".nh" ) . forEach ( ( el ) =>
70- el . addEventListener ( "click" , ( ) => {
71- el . lastChild . click ( ) ;
72- el . first . addClass ( "expanded" ) ;
73- el . parent . addClass ( "expanded" ) ;
74- } ) ,
75- ) ;
100+ document . querySelectorAll ( ".nh" ) . forEach ( el => el . addEventListener ( 'click' , ( ) => {
101+ if ( el . lastChild . href . replace ( "#" , "" ) === window . location . href . replace ( "#" , "" ) ) {
102+ el . parentElement . classList . toggle ( "expanded" )
103+ el . firstChild . classList . toggle ( "expanded" )
104+ } else {
105+ el . lastChild . click ( )
106+ }
107+ } ) )
76108
77109 document . querySelectorAll ( ".supertypes" ) . forEach ( ( el ) =>
78110 el . firstChild . addEventListener ( "click" , ( ) => {
@@ -120,8 +152,6 @@ window.addEventListener("DOMContentLoaded", () => {
120152 observer . observe ( section ) ;
121153 } ) ;
122154
123- document . querySelectorAll ( ".side-menu a" ) . forEach ( elem => elem . addEventListener ( 'click' , e => e . stopPropagation ( ) ) )
124-
125155 if ( location . hash ) {
126156 var target = location . hash . substring ( 1 ) ;
127157 // setting the 'expand' class on the top-level container causes undesireable styles
@@ -134,28 +164,9 @@ window.addEventListener("DOMContentLoaded", () => {
134164 }
135165 }
136166
137- var logo = document . getElementById ( "logo" ) ;
138- if ( logo ) {
139- logo . onclick = function ( ) {
140- window . location = pathToRoot ; // global variable pathToRoot is created by the html renderer
141- } ;
142- }
143-
144- document . querySelectorAll ( '.documentableAnchor' ) . forEach ( elem => {
145- elem . addEventListener ( 'click' , event => {
146- var $temp = $ ( "<input>" )
147- $ ( "body" ) . append ( $temp )
148- var a = document . createElement ( 'a' )
149- a . href = $ ( elem ) . attr ( "link" )
150- $temp . val ( a . href ) . select ( ) ;
151- document . execCommand ( "copy" )
152- $temp . remove ( ) ;
153- } )
154- } )
155-
156- hljs . registerLanguage ( "scala" , highlightDotty ) ;
157- hljs . registerAliases ( [ "dotty" , "scala3" ] , "scala" ) ;
158- hljs . initHighlighting ( ) ;
167+ document . querySelectorAll ( 'pre code' ) . forEach ( el => {
168+ hljs . highlightBlock ( el ) ;
169+ } ) ;
159170
160171 /* listen for the `F` key to be pressed, to focus on the member filter input (if it's present) */
161172 document . body . addEventListener ( 'keydown' , e => {
@@ -171,32 +182,44 @@ window.addEventListener("DOMContentLoaded", () => {
171182 }
172183 } )
173184
174- // show/hide side menu on mobile view
175- const sideMenuToggler = document . getElementById ( "mobile-sidebar-toggle" ) ;
176- sideMenuToggler . addEventListener ( 'click' , _e => {
177- document . getElementById ( "leftColumn" ) . classList . toggle ( "show" )
178- document . getElementById ( "content" ) . classList . toggle ( "sidebar-shown" )
179- const toc = document . getElementById ( "toc" ) ;
180- if ( toc ) {
181- toc . classList . toggle ( "sidebar-shown" )
182- }
183- sideMenuToggler . classList . toggle ( "menu-shown" )
184- } )
185-
186- // show/hide mobile menu on mobile view
187- const mobileMenuOpenIcon = document . getElementById ( "mobile-menu-toggle" ) ;
188- const mobileMenuCloseIcon = document . getElementById ( "mobile-menu-close" ) ;
189- mobileMenuOpenIcon . addEventListener ( 'click' , _e => {
190- document . getElementById ( "mobile-menu" ) . classList . add ( "show" )
191- } )
192- mobileMenuCloseIcon . addEventListener ( 'click' , _e => {
193- document . getElementById ( "mobile-menu" ) . classList . remove ( "show" )
194- } )
195-
196-
197185 // when document is loaded graph needs to be shown
186+ }
187+
188+ window . addEventListener ( "DOMContentLoaded" , ( ) => {
189+ hljs . registerLanguage ( "scala" , highlightDotty ) ;
190+ hljs . registerAliases ( [ "dotty" , "scala3" ] , "scala" ) ;
191+ attachAllListeners ( )
198192} ) ;
199193
194+ // show/hide side menu on mobile view
195+ const sideMenuToggler = document . getElementById ( "mobile-sidebar-toggle" )
196+ sideMenuToggler . addEventListener ( 'click' , _e => {
197+ document . getElementById ( "leftColumn" ) . classList . toggle ( "show" )
198+ document . getElementById ( "content" ) . classList . toggle ( "sidebar-shown" )
199+ const toc = document . getElementById ( "toc" ) ;
200+ if ( toc && toc . childElementCount > 0 ) {
201+ toc . classList . toggle ( "sidebar-shown" )
202+ }
203+ sideMenuToggler . classList . toggle ( "menu-shown" )
204+ } )
205+
206+ // show/hide mobile menu on mobile view
207+ document . getElementById ( "mobile-menu-toggle" ) . addEventListener ( 'click' , _e => {
208+ document . getElementById ( "mobile-menu" ) . classList . add ( "show" )
209+ } )
210+ document . getElementById ( "mobile-menu-close" ) . addEventListener ( 'click' , _e => {
211+ document . getElementById ( "mobile-menu" ) . classList . remove ( "show" )
212+ } )
213+
214+ window . addEventListener ( 'popstate' , e => {
215+ const { leftColumn, mainDiv, title } = e . state
216+ document . title = title
217+ const { children } = document . body . firstChild
218+ children [ 3 ] . innerHTML = leftColumn
219+ children [ 6 ] . innerHTML = mainDiv
220+ attachAllListeners ( )
221+ } )
222+
200223var zoom ;
201224var transform ;
202225
0 commit comments