src/Pure/PIDE/command_span.scala
author wenzelm
Sat, 10 Dec 2022 21:02:09 +0100
changeset 76615 b865959e2547
parent 75393 87ebf5a50283
child 76798 69d8d16c5612
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/PIDE/command_span.scala
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     3
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     4
Syntactic representation of command spans.
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     5
*/
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     6
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     7
package isabelle
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     8
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     9
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    10
import scala.collection.mutable
72946
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 72816
diff changeset
    11
import scala.util.parsing.input.CharSequenceReader
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    12
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    13
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74671
diff changeset
    14
object Command_Span {
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    15
  /* loaded files */
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    16
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74671
diff changeset
    17
  object Loaded_Files {
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    18
    val none: Loaded_Files = Loaded_Files(Nil, -1)
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    19
  }
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    20
  sealed case class Loaded_Files(files: List[String], index: Int)
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    21
74671
df12779c3ce8 more PIDE markup;
wenzelm
parents: 73359
diff changeset
    22
  abstract class Load_Command(val name: String, val here: Scala_Project.Here)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74671
diff changeset
    23
  extends Isabelle_System.Service {
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    24
    override def toString: String = name
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    25
74671
df12779c3ce8 more PIDE markup;
wenzelm
parents: 73359
diff changeset
    26
    def position: Position.T = here.position
df12779c3ce8 more PIDE markup;
wenzelm
parents: 73359
diff changeset
    27
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    28
    def extensions: List[String] = Nil
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    29
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    30
    def loaded_files(tokens: List[(Token, Int)]): Loaded_Files =
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    31
      tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match {
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    32
        case Some((file, i)) =>
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    33
          extensions match {
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    34
            case Nil => Loaded_Files(List(file), i)
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    35
            case exts => Loaded_Files(exts.map(ext => file + "." + ext), i)
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    36
          }
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    37
        case None => Loaded_Files.none
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    38
      }
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    39
  }
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    40
76615
b865959e2547 tuned signature;
wenzelm
parents: 75393
diff changeset
    41
  object Load_Default extends Load_Command("", Scala_Project.here)
74671
df12779c3ce8 more PIDE markup;
wenzelm
parents: 73359
diff changeset
    42
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    43
  lazy val load_commands: List[Load_Command] =
76615
b865959e2547 tuned signature;
wenzelm
parents: 75393
diff changeset
    44
    Load_Default :: Isabelle_System.make_services(classOf[Load_Command])
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    45
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    46
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    47
  /* span kind */
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    48
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    49
  sealed abstract class Kind {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    50
    override def toString: String =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    51
      this match {
73115
a8e5d7c9a834 discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it violates translation invariance of commands and may lead to redundant re-checking of PIDE document;
wenzelm
parents: 72946
diff changeset
    52
        case Command_Span(name, _) => proper_string(name) getOrElse "<command>"
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    53
        case Ignored_Span => "<ignored>"
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    54
        case Malformed_Span => "<malformed>"
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
    55
        case Theory_Span => "<theory>"
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    56
      }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    57
  }
73115
a8e5d7c9a834 discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it violates translation invariance of commands and may lead to redundant re-checking of PIDE document;
wenzelm
parents: 72946
diff changeset
    58
  case class Command_Span(name: String, pos: Position.T) extends Kind
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    59
  case object Ignored_Span extends Kind
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    60
  case object Malformed_Span extends Kind
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
    61
  case object Theory_Span extends Kind
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    62
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    63
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    64
  /* span */
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    65
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74671
diff changeset
    66
  sealed case class Span(kind: Kind, content: List[Token]) {
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
    67
    def is_theory: Boolean = kind == Theory_Span
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
    68
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
    69
    def name: String =
72800
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    70
      kind match { case k: Command_Span => k.name case _ => "" }
58802
3cc68ec558b0 find command span in buffer;
wenzelm
parents: 57910
diff changeset
    71
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
    72
    def position: Position.T =
72800
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    73
      kind match { case k: Command_Span => k.pos case _ => Position.none }
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    74
67895
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    75
    def keyword_pos(start: Token.Pos): Token.Pos =
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    76
      kind match {
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    77
        case _: Command_Span =>
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73115
diff changeset
    78
          content.iterator.takeWhile(tok => !tok.is_command).foldLeft(start)(_.advance(_))
67895
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    79
        case _ => start
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    80
      }
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    81
68845
3b2daa7bf9f4 support Thy_Element in Scala, following ML version;
wenzelm
parents: 68840
diff changeset
    82
    def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean =
68840
51ab4c78235b tuned signature;
wenzelm
parents: 67895
diff changeset
    83
      keywords.kinds.get(name) match {
51ab4c78235b tuned signature;
wenzelm
parents: 67895
diff changeset
    84
        case Some(k) => pred(k)
68845
3b2daa7bf9f4 support Thy_Element in Scala, following ML version;
wenzelm
parents: 68840
diff changeset
    85
        case None => other
68840
51ab4c78235b tuned signature;
wenzelm
parents: 67895
diff changeset
    86
      }
51ab4c78235b tuned signature;
wenzelm
parents: 67895
diff changeset
    87
63606
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    88
    def is_begin: Boolean = content.exists(_.is_begin)
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    89
    def is_end: Boolean = content.exists(_.is_end)
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    90
72946
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 72816
diff changeset
    91
    def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 72816
diff changeset
    92
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73115
diff changeset
    93
    def length: Int = content.foldLeft(0)(_ + _.source.length)
59705
740a0ca7e09b clarified span position;
wenzelm
parents: 59689
diff changeset
    94
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74671
diff changeset
    95
    def compact_source: (String, Span) = {
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
    96
      val source = Token.implode(content)
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    97
      val content1 = new mutable.ListBuffer[Token]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    98
      var i = 0
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    99
      for (Token(kind, s) <- content) {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   100
        val n = s.length
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
   101
        val s1 = source.substring(i, i + n)
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   102
        content1 += Token(kind, s1)
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   103
        i += n
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   104
      }
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
   105
      (source, Span(kind, content1.toList))
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   106
    }
72742
bda424c5819f clarified modules;
wenzelm
parents: 72692
diff changeset
   107
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74671
diff changeset
   108
    def clean_arguments: List[(Token, Int)] = {
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   109
      if (name.nonEmpty) {
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   110
        def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   111
          toks match {
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   112
            case (t1, i1) :: (t2, i2) :: rest =>
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   113
              if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   114
              else (t1, i1) :: clean((t2, i2) :: rest)
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   115
            case _ => toks
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   116
          }
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   117
        clean(content.zipWithIndex.filter({ case (t, _) => t.is_proper }))
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   118
          .dropWhile({ case (t, _) => !t.is_command })
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   119
          .dropWhile({ case (t, _) => t.is_command })
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   120
      }
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   121
      else Nil
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   122
    }
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   123
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72800
diff changeset
   124
    def is_load_command(syntax: Outer_Syntax): Boolean =
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72800
diff changeset
   125
      syntax.load_command(name).isDefined
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72800
diff changeset
   126
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   127
    def loaded_files(syntax: Outer_Syntax): Loaded_Files =
72742
bda424c5819f clarified modules;
wenzelm
parents: 72692
diff changeset
   128
      syntax.load_command(name) match {
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
   129
        case None => Loaded_Files.none
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   130
        case Some(a) =>
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   131
          load_commands.find(_.name == a) match {
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   132
            case Some(load_command) => load_command.loaded_files(clean_arguments)
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   133
            case None => error("Undefined load command function: " + a)
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   134
          }
72742
bda424c5819f clarified modules;
wenzelm
parents: 72692
diff changeset
   135
      }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   136
  }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   137
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   138
  val empty: Span = Span(Ignored_Span, Nil)
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   139
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74671
diff changeset
   140
  def unparsed(source: String, theory: Boolean): Span = {
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
   141
    val kind = if (theory) Theory_Span else Malformed_Span
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
   142
    Span(kind, List(Token(Token.Kind.UNPARSED, source)))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
   143
  }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   144
}