tuned;
authorwenzelm
Fri May 11 20:22:20 2018 +0200 (12 months ago)
changeset 681513c321783bae3
parent 68150 f0f34cbed539
child 68152 619de043389f
tuned;
src/Pure/Thy/export.scala
     1.1 --- a/src/Pure/Thy/export.scala	Fri May 11 20:05:37 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Fri May 11 20:22:20 2018 +0200
     1.3 @@ -104,6 +104,13 @@
     1.4      make(Nil, 0, pattern.toList)
     1.5    }
     1.6  
     1.7 +  def make_matcher(pattern: String): (String, String) => Boolean =
     1.8 +  {
     1.9 +    val regex = make_regex(pattern)
    1.10 +    (theory_name: String, name: String) =>
    1.11 +      regex.pattern.matcher(compound_name(theory_name, name)).matches
    1.12 +  }
    1.13 +
    1.14    def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
    1.15    {
    1.16      Entry(session_name, args.theory_name, args.name, args.compress,
    1.17 @@ -255,11 +262,9 @@
    1.18  
    1.19          // export
    1.20          if (export_pattern != "") {
    1.21 -          val regex = make_regex(export_pattern)
    1.22 -          for {
    1.23 -            (theory_name, name) <- export_names
    1.24 -            if regex.pattern.matcher(compound_name(theory_name, name)).matches
    1.25 -          } {
    1.26 +          val matcher = make_matcher(export_pattern)
    1.27 +          for { (theory_name, name) <- export_names if matcher(theory_name, name) }
    1.28 +          {
    1.29              val entry = read_entry(db, session_name, theory_name, name)
    1.30              val path = export_dir + Path.basic(theory_name) + Path.explode(name)
    1.31