# HG changeset patch
# User wenzelm
# Date 1606654758 -3600
# Node ID 0c86c29767b2d7e8a357b8d5698b1e81ca01bf50
# Parent  f6bf655547646b0ec78d9997bcee28f2494649ed
tuned;

diff -r f6bf65554764 -r 0c86c29767b2 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sat Nov 28 23:36:17 2020 +0100
+++ b/src/Pure/Tools/doc.scala	Sun Nov 29 13:59:18 2020 +0100
@@ -7,9 +7,6 @@
 package isabelle
 
 
-import scala.util.matching.Regex
-
-
 object Doc
 {
   /* dirs */
@@ -41,8 +38,8 @@
     }
     else None
 
-  private val Section_Entry = new Regex("""^(\S.*)\s*$""")
-  private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
+  private val Section_Entry = """^(\S.*)\s*$""".r
+  private val Doc_Entry = """^\s+(\S+)\s+(.+)\s*$""".r
 
   private def release_notes(): List[Entry] =
     Section("Release Notes", true) ::