--- a/src/Pure/PIDE/document.scala Thu Feb 20 15:15:41 2014 +0100
+++ b/src/Pure/PIDE/document.scala Thu Feb 20 16:00:37 2014 +0100
@@ -369,11 +369,11 @@
def cumulate_markup[A](
range: Text.Range,
info: A,
- elements: Option[Set[String]],
+ elements: String => Boolean,
result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
def select_markup[A](
range: Text.Range,
- elements: Option[Set[String]],
+ elements: String => Boolean,
result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
}
@@ -629,7 +629,7 @@
(thy_load_commands zip other.thy_load_commands).forall(eq_commands)
}
- def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
+ def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
val former_range = revert(range)
@@ -659,7 +659,7 @@
}
}
- def select_markup[A](range: Text.Range, elements: Option[Set[String]],
+ def select_markup[A](range: Text.Range, elements: String => Boolean,
result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
{
def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
@@ -671,7 +671,7 @@
case some => Some(some)
}
}
- for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
+ for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
yield Text.Info(r, x)
}
}