--- 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) ::