src/Pure/PIDE/command_span.scala
author wenzelm
Tue, 01 Dec 2020 20:47:03 +0100
changeset 72800 85bcdd05c6d0
parent 72757 38e05b7ded61
child 72816 ea4f86914cb2
permissions -rw-r--r--
clarified signature --- more positions;
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
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    11
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
object Command_Span
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    14
{
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    15
  /* loaded files */
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    16
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    17
  object Loaded_Files
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    18
  {
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    19
    val none: Loaded_Files = Loaded_Files(Nil, -1)
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    20
  }
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    21
  sealed case class Loaded_Files(files: List[String], index: Int)
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    22
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    23
  class Load_Command(val name: String) extends Isabelle_System.Service
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    24
  {
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    25
    override def toString: String = name
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    26
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    27
    def extensions: List[String] = Nil
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    28
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    29
    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
    30
      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
    31
        case Some((file, i)) =>
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    32
          extensions match {
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    33
            case Nil => Loaded_Files(List(file), i)
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    34
            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
    35
          }
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
    36
        case None => Loaded_Files.none
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    37
      }
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
  lazy val load_commands: List[Load_Command] =
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
    41
    new Load_Command("") :: Isabelle_System.make_services(classOf[Load_Command])
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    42
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    43
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    44
  /* span kind */
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    45
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    46
  sealed abstract class Kind {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    47
    override def toString: String =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    48
      this match {
72800
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    49
        case Command_Span(name, _, _) => proper_string(name) getOrElse "<command>"
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    50
        case Ignored_Span => "<ignored>"
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    51
        case Malformed_Span => "<malformed>"
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
    52
        case Theory_Span => "<theory>"
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    53
      }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    54
  }
72800
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    55
  case class Command_Span(name: String, pos: Position.T, abs_pos: Position.T) extends Kind
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    56
  case object Ignored_Span extends Kind
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    57
  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
    58
  case object Theory_Span extends Kind
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    59
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    60
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    61
  /* span */
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
    62
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    63
  sealed case class Span(kind: Kind, content: List[Token])
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    64
  {
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
    65
    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
    66
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
    67
    def name: String =
72800
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    68
      kind match { case k: Command_Span => k.name case _ => "" }
58802
3cc68ec558b0 find command span in buffer;
wenzelm
parents: 57910
diff changeset
    69
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
    70
    def position: Position.T =
72800
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    71
      kind match { case k: Command_Span => k.pos case _ => Position.none }
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    72
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    73
    def absolute_position: Position.T =
85bcdd05c6d0 clarified signature --- more positions;
wenzelm
parents: 72757
diff changeset
    74
      kind match { case k: Command_Span => k.abs_pos case _ => Position.none }
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
    75
67895
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    76
    def keyword_pos(start: Token.Pos): Token.Pos =
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    77
      kind match {
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    78
        case _: Command_Span =>
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    79
          (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_))
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    80
        case _ => start
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    81
      }
cd00999d2d30 more position information;
wenzelm
parents: 65717
diff changeset
    82
68845
3b2daa7bf9f4 support Thy_Element in Scala, following ML version;
wenzelm
parents: 68840
diff changeset
    83
    def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean =
68840
51ab4c78235b tuned signature;
wenzelm
parents: 67895
diff changeset
    84
      keywords.kinds.get(name) match {
51ab4c78235b tuned signature;
wenzelm
parents: 67895
diff changeset
    85
        case Some(k) => pred(k)
68845
3b2daa7bf9f4 support Thy_Element in Scala, following ML version;
wenzelm
parents: 68840
diff changeset
    86
        case None => other
68840
51ab4c78235b tuned signature;
wenzelm
parents: 67895
diff changeset
    87
      }
51ab4c78235b tuned signature;
wenzelm
parents: 67895
diff changeset
    88
63606
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    89
    def is_begin: Boolean = content.exists(_.is_begin)
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    90
    def is_end: Boolean = content.exists(_.is_end)
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    91
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59705
diff changeset
    92
    def length: Int = (0 /: content)(_ + _.source.length)
59705
740a0ca7e09b clarified span position;
wenzelm
parents: 59689
diff changeset
    93
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    94
    def compact_source: (String, Span) =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    95
    {
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
72743
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   108
    def clean_arguments: List[(Token, Int)] =
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   109
    {
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   110
      if (name.nonEmpty) {
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   111
        def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   112
          toks match {
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   113
            case (t1, i1) :: (t2, i2) :: rest =>
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   114
              if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   115
              else (t1, i1) :: clean((t2, i2) :: rest)
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   116
            case _ => toks
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   117
          }
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   118
        clean(content.zipWithIndex.filter({ case (t, _) => t.is_proper }))
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   119
          .dropWhile({ case (t, _) => !t.is_command })
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   120
          .dropWhile({ case (t, _) => t.is_command })
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   121
      }
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   122
      else Nil
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   123
    }
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   124
bc82fc605424 clarified signature;
wenzelm
parents: 72742
diff changeset
   125
    def loaded_files(syntax: Outer_Syntax): Loaded_Files =
72742
bda424c5819f clarified modules;
wenzelm
parents: 72692
diff changeset
   126
      syntax.load_command(name) match {
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
   127
        case None => Loaded_Files.none
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   128
        case Some(a) =>
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   129
          load_commands.find(_.name == a) match {
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   130
            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
   131
            case None => error("Undefined load command function: " + a)
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72744
diff changeset
   132
          }
72742
bda424c5819f clarified modules;
wenzelm
parents: 72692
diff changeset
   133
      }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   134
  }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   135
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   136
  val empty: Span = Span(Ignored_Span, Nil)
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   137
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
   138
  def unparsed(source: String, theory: Boolean): Span =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
   139
  {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 68845
diff changeset
   140
    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
   141
    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
   142
  }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
   143
}