···

       
524
       
524
       
 
       
    const hash = location.hash;

     

       
525
       
525
       
 
       
    if (hash.startsWith("#schema:")) {

     

       
526
       
526
       
 
       
      const defName = hash.slice(8);

     

       
527
       
527
       
-
       
      setTimeout(() => {

     

       
528
       
528
       
-
       
        const element = document.getElementById(`def-${defName}`);

     

       
529
       
529
       
-
       
        if (element) {

     

       
530
       
530
       
-
       
          element.scrollIntoView({ behavior: "instant", block: "start" });

     

       
531
       
531
       
-
       
        }

     

       
532
       
532
       
-
       
      }, 100);

     

       
527
       
527
       
+
       
      const element = document.getElementById(`def-${defName}`);

     

       
528
       
528
       
+
       
      if (element) element.scrollIntoView({ behavior: "instant", block: "start" });

     

       
533
       
529
       
 
       
    }

     

       
534
       
530
       
 
       
  });

     

       
535
       
531