# HG changeset patch
# User wenzelm
# Date 1606473703 -3600
# Node ID 082200ee003d60a3e6028600d6c0fac0777b8682
# Parent  a4d7da18ac5cd8172f7fb62f392d6ee604fcdaa5
tuned signature;

diff -r a4d7da18ac5c -r 082200ee003d src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Thu Nov 26 23:23:19 2020 +0100
+++ b/src/Pure/Isar/keyword.scala	Fri Nov 27 11:41:43 2020 +0100
@@ -208,12 +208,6 @@
       token.is_begin_or_command || is_quasi_command(token)
 
 
-    /* load commands */
-
-    def load_commands_in(text: String): Boolean =
-      load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
-
-
     /* lexicons */
 
     private def make_lexicon(is_minor: Boolean): Scan.Lexicon =
diff -r a4d7da18ac5c -r 082200ee003d src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Thu Nov 26 23:23:19 2020 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Fri Nov 27 11:41:43 2020 +0100
@@ -133,8 +133,11 @@
 
   /* load commands */
 
-  def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
-  def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
+  def load_command(name: String): Option[List[String]] =
+    keywords.load_commands.get(name)
+
+  def has_load_commands(text: String): Boolean =
+    keywords.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
 
 
   /* language context */
diff -r a4d7da18ac5c -r 082200ee003d src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Nov 26 23:23:19 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Nov 27 11:41:43 2020 +0100
@@ -113,7 +113,7 @@
     val (is_utf8, raw_text) =
       with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString))
     () => {
-      if (syntax.load_commands_in(raw_text)) {
+      if (syntax.has_load_commands(raw_text)) {
         val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
         val spans = syntax.parse_spans(text)
         val dir = Path.explode(name.master_dir)