--- a/src/Pure/Isar/outer_syntax.scala Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Thu Apr 03 20:53:35 2014 +0200
@@ -44,7 +44,7 @@
lexicon: Scan.Lexicon = Scan.Lexicon.empty,
val completion: Completion = Completion.empty,
val language_context: Completion.Language_Context = Completion.Language_Context.outer,
- val has_tokens: Boolean = true)
+ val has_tokens: Boolean = true) extends Prover.Syntax
{
override def toString: String =
(for ((name, (kind, files)) <- keywords) yield {
@@ -66,6 +66,9 @@
val load_commands: List[(String, List[String])] =
(for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
+ def load_commands_in(text: String): Boolean =
+ load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
{
val keywords1 = keywords + (name -> kind)