tuned signature;
authorwenzelm
Fri, 27 Nov 2020 11:41:43 +0100
changeset 72978 082200ee003d
parent 72975 a4d7da18ac5c
child 72979 b808eddc83cf
tuned signature;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/resources.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 =
--- 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)