--- 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 =
--- 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 */
--- 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)