# HG changeset patch
# User wenzelm
# Date 1526062940 -7200
# Node ID 3c321783bae31048a9e8c9d551db3af09b5e44aa
# Parent  f0f34cbed5396b6215fc37f5ded5d39031e520be
tuned;

diff -r f0f34cbed539 -r 3c321783bae3 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri May 11 20:05:37 2018 +0200
+++ b/src/Pure/Thy/export.scala	Fri May 11 20:22:20 2018 +0200
@@ -104,6 +104,13 @@
     make(Nil, 0, pattern.toList)
   }
 
+  def make_matcher(pattern: String): (String, String) => Boolean =
+  {
+    val regex = make_regex(pattern)
+    (theory_name: String, name: String) =>
+      regex.pattern.matcher(compound_name(theory_name, name)).matches
+  }
+
   def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
   {
     Entry(session_name, args.theory_name, args.name, args.compress,
@@ -255,11 +262,9 @@
 
         // export
         if (export_pattern != "") {
-          val regex = make_regex(export_pattern)
-          for {
-            (theory_name, name) <- export_names
-            if regex.pattern.matcher(compound_name(theory_name, name)).matches
-          } {
+          val matcher = make_matcher(export_pattern)
+          for { (theory_name, name) <- export_names if matcher(theory_name, name) }
+          {
             val entry = read_entry(db, session_name, theory_name, name)
             val path = export_dir + Path.basic(theory_name) + Path.explode(name)