src/Pure/Isar/outer_syntax.scala
author wenzelm
Tue, 04 Apr 2017 22:53:01 +0200
changeset 65383 089f2edefb77
parent 64616 dc3ec40fe41b
child 65384 36255c43c64c
permissions -rw-r--r--
proper name according to meaning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Isar/outer_syntax.scala
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     3
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     4
Isabelle/Isar outer syntax.
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     5
*/
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     6
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     7
package isabelle
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     8
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     9
43411
0206466ee473 some support for partial scans with explicit context;
wenzelm
parents: 40533
diff changeset
    10
import scala.collection.mutable
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    11
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    12
43774
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    13
object Outer_Syntax
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    14
{
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    15
  /* syntax */
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    16
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    17
  val empty: Outer_Syntax = new Outer_Syntax()
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    18
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    19
  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    20
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    21
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    22
  /* string literals */
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    23
43774
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    24
  def quote_string(str: String): String =
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    25
  {
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    26
    val result = new StringBuilder(str.length + 10)
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    27
    result += '"'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    28
    for (s <- Symbol.iterator(str)) {
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    29
      if (s.length == 1) {
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    30
        val c = s(0)
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    31
        if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    32
          result += '\\'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    33
          if (c < 10) result += '0'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    34
          if (c < 100) result += '0'
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59939
diff changeset
    35
          result ++= c.asInstanceOf[Int].toString
43774
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    36
        }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    37
        else result += c
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    38
      }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    39
      else result ++= s
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    40
    }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    41
    result += '"'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    42
    result.toString
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    43
  }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    44
}
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    45
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46626
diff changeset
    46
final class Outer_Syntax private(
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
    47
  val keywords: Keyword.Keywords = Keyword.Keywords.empty,
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
    48
  val completion: Completion = Completion.empty,
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    49
  val rev_abbrevs: Thy_Header.Abbrevs = Nil,
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
    50
  val language_context: Completion.Language_Context = Completion.Language_Context.outer,
63584
68751fe1c036 tuned signature -- prover-independence is presently theoretical;
wenzelm
parents: 63579
diff changeset
    51
  val has_tokens: Boolean = true)
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    52
{
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    53
  /** syntax content **/
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    54
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
    55
  override def toString: String = keywords.toString
56393
22f533e6a049 more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents: 56314
diff changeset
    56
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    57
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    58
  /* keywords */
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    59
65383
089f2edefb77 proper name according to meaning;
wenzelm
parents: 64616
diff changeset
    60
  def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
    61
  {
65383
089f2edefb77 proper name according to meaning;
wenzelm
parents: 64616
diff changeset
    62
    val keywords1 = keywords + (name, kind, exts)
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
    63
    val completion1 =
63587
881e8e2cfec2 implicit keyword completion only for actual words (amending 73939a9b70a3);
wenzelm
parents: 63584
diff changeset
    64
      completion.add_keyword(name).
881e8e2cfec2 implicit keyword completion only for actual words (amending 73939a9b70a3);
wenzelm
parents: 63584
diff changeset
    65
        add_abbrevs(
881e8e2cfec2 implicit keyword completion only for actual words (amending 73939a9b70a3);
wenzelm
parents: 63584
diff changeset
    66
          (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
881e8e2cfec2 implicit keyword completion only for actual words (amending 73939a9b70a3);
wenzelm
parents: 63584
diff changeset
    67
           else Nil) :::
881e8e2cfec2 implicit keyword completion only for actual words (amending 73939a9b70a3);
wenzelm
parents: 63584
diff changeset
    68
          (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    69
    new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
    70
  }
48706
e2b512024eab tuned signature;
wenzelm
parents: 48671
diff changeset
    71
48873
18b17f15bc62 more direct cumulation of (sparse) keywords;
wenzelm
parents: 48872
diff changeset
    72
  def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
18b17f15bc62 more direct cumulation of (sparse) keywords;
wenzelm
parents: 48872
diff changeset
    73
    (this /: keywords) {
65383
089f2edefb77 proper name according to meaning;
wenzelm
parents: 64616
diff changeset
    74
      case (syntax, (name, ((kind, exts), _))) =>
089f2edefb77 proper name according to meaning;
wenzelm
parents: 64616
diff changeset
    75
        syntax + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    76
    }
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    77
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    78
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    79
  /* abbrevs */
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    80
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    81
  def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    82
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    83
  def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    84
    if (new_abbrevs.isEmpty) this
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    85
    else {
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    86
      val completion1 =
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    87
        completion.add_abbrevs(
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    88
          (for ((a, b) <- new_abbrevs) yield {
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    89
            val a1 = Symbol.decode(a)
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    90
            val a2 = Symbol.encode(a)
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    91
            val b1 = Symbol.decode(b)
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    92
            List((a1, b1), (a2, b1))
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63528
diff changeset
    93
          }).flatten)
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    94
      val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
    95
      new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens)
46940
a40be2f10ca9 explicit Outer_Syntax.Decl;
wenzelm
parents: 46712
diff changeset
    96
    }
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    97
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    98
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
    99
  /* merge */
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   100
63584
68751fe1c036 tuned signature -- prover-independence is presently theoretical;
wenzelm
parents: 63579
diff changeset
   101
  def ++ (other: Outer_Syntax): Outer_Syntax =
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   102
    if (this eq other) this
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   103
    else {
63865
wenzelm
parents: 63604
diff changeset
   104
      val keywords1 = keywords ++ other.keywords
wenzelm
parents: 63604
diff changeset
   105
      val completion1 = completion ++ other.completion
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
   106
      val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59073
diff changeset
   107
      if ((keywords eq keywords1) && (completion eq completion1)) this
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
   108
      else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   109
    }
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   110
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   111
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   112
  /* load commands */
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   113
63441
4c3fa4dba79f explicit kind "before_command";
wenzelm
parents: 63429
diff changeset
   114
  def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   115
  def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   116
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   117
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   118
  /* language context */
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   119
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   120
  def set_language_context(context: Completion.Language_Context): Outer_Syntax =
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
   121
    new Outer_Syntax(keywords, completion, rev_abbrevs, context, has_tokens)
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   122
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   123
  def no_tokens: Outer_Syntax =
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   124
  {
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   125
    require(keywords.is_empty)
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   126
    new Outer_Syntax(
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   127
      completion = completion,
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63865
diff changeset
   128
      rev_abbrevs = rev_abbrevs,
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   129
      language_context = language_context,
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   130
      has_tokens = false)
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   131
  }
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   132
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   133
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   134
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   135
  /** parsing **/
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   136
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   137
  /* command spans */
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   138
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   139
  def parse_spans(toks: List[Token]): List[Command_Span.Span] =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   140
  {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   141
    val result = new mutable.ListBuffer[Command_Span.Span]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   142
    val content = new mutable.ListBuffer[Token]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   143
    val improper = new mutable.ListBuffer[Token]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   144
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   145
    def ship(span: List[Token])
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   146
    {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   147
      val kind =
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   148
        if (span.forall(_.is_improper)) Command_Span.Ignored_Span
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   149
        else if (span.exists(_.is_error)) Command_Span.Malformed_Span
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   150
        else
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   151
          span.find(_.is_command) match {
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   152
            case None => Command_Span.Malformed_Span
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   153
            case Some(cmd) =>
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   154
              val name = cmd.source
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   155
              val offset =
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   156
                (0 /: span.takeWhile(_ != cmd)) {
64616
wenzelm
parents: 63867
diff changeset
   157
                  case (i, tok) => i + Symbol.length(tok.source) }
wenzelm
parents: 63867
diff changeset
   158
              val end_offset = offset + Symbol.length(name)
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   159
              val pos = Position.Range(Text.Range(offset, end_offset) + 1)
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   160
              Command_Span.Command_Span(name, pos)
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   161
          }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   162
      result += Command_Span.Span(kind, span)
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   163
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   164
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   165
    def flush()
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   166
    {
59319
wenzelm
parents: 59122
diff changeset
   167
      if (content.nonEmpty) { ship(content.toList); content.clear }
wenzelm
parents: 59122
diff changeset
   168
      if (improper.nonEmpty) { ship(improper.toList); improper.clear }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   169
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   170
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   171
    for (tok <- toks) {
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   172
      if (tok.is_improper) improper += tok
63441
4c3fa4dba79f explicit kind "before_command";
wenzelm
parents: 63429
diff changeset
   173
      else if (keywords.is_before_command(tok) ||
4c3fa4dba79f explicit kind "before_command";
wenzelm
parents: 63429
diff changeset
   174
        tok.is_command &&
4c3fa4dba79f explicit kind "before_command";
wenzelm
parents: 63429
diff changeset
   175
          (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   176
      { flush(); content += tok }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   177
      else { content ++= improper; improper.clear; content += tok }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   178
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   179
    flush()
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   180
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   181
    result.toList
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   182
  }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   183
57906
020df63dd0a9 tuned signature;
wenzelm
parents: 57905
diff changeset
   184
  def parse_spans(input: CharSequence): List[Command_Span.Span] =
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59077
diff changeset
   185
    parse_spans(Token.explode(keywords, input))
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   186
}