src/Pure/Isar/outer_syntax.scala
author wenzelm
Wed, 08 Jul 2015 15:37:32 +0200
changeset 60694 b3fa4a8cdb5f
parent 60692 896704918a1f
child 61463 8e46cea6a45a
permissions -rw-r--r--
clarified text folds: proof ... qed counts as extra block;
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
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    11
import scala.annotation.tailrec
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    12
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    13
43774
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    14
object Outer_Syntax
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    15
{
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    16
  /* syntax */
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    17
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    18
  val empty: Outer_Syntax = new Outer_Syntax()
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    19
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    20
  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    21
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    22
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    23
  /* string literals */
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    24
43774
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    25
  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
    26
  {
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    27
    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
    28
    result += '"'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    29
    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
    30
      if (s.length == 1) {
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    31
        val c = s(0)
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    32
        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
    33
          result += '\\'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    34
          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
    35
          if (c < 100) result += '0'
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59939
diff changeset
    36
          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
    37
        }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    38
        else result += c
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    39
      }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    40
      else result ++= s
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    41
    }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    42
    result += '"'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    43
    result.toString
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    44
  }
46626
a02115865bcc streamlined abstract datatype;
wenzelm
parents: 46624
diff changeset
    45
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    46
58697
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
    47
  /* line-oriented structure */
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    48
58697
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
    49
  object Line_Structure
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    50
  {
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    51
    val init = Line_Structure()
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    52
  }
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    53
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    54
  sealed case class Line_Structure(
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    55
    improper: Boolean = true,
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    56
    command: Boolean = false,
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    57
    depth: Int = 0,
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    58
    span_depth: Int = 0,
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    59
    after_span_depth: Int = 0)
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    60
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    61
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    62
  /* overall document structure */
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    63
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    64
  sealed abstract class Document { def length: Int }
58747
c680f181b32e tuned rendering;
wenzelm
parents: 58743
diff changeset
    65
  case class Document_Block(name: String, text: String, body: List[Document]) extends Document
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    66
  {
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    67
    val length: Int = (0 /: body)(_ + _.length)
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    68
  }
58747
c680f181b32e tuned rendering;
wenzelm
parents: 58743
diff changeset
    69
  case class Document_Atom(command: Command) extends Document
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    70
  {
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    71
    def length: Int = command.length
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    72
  }
43774
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    73
}
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    74
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46626
diff changeset
    75
final class Outer_Syntax private(
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
    76
  val keywords: Keyword.Keywords = Keyword.Keywords.empty,
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
    77
  val completion: Completion = Completion.empty,
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
    78
  val language_context: Completion.Language_Context = Completion.Language_Context.outer,
56393
22f533e6a049 more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents: 56314
diff changeset
    79
  val has_tokens: Boolean = true) extends Prover.Syntax
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    80
{
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    81
  /** syntax content **/
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
    82
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
    83
  override def toString: String = keywords.toString
56393
22f533e6a049 more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents: 56314
diff changeset
    84
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    85
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    86
  /* add keywords */
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    87
58907
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58901
diff changeset
    88
  def + (name: String): Outer_Syntax = this + (name, None, None)
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58901
diff changeset
    89
  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
58901
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
    90
  def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
    91
    : Outer_Syntax =
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
    92
  {
58901
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
    93
    val keywords1 =
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
    94
      opt_kind match {
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
    95
        case None => keywords + name
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
    96
        case Some(kind) => keywords + (name, kind)
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
    97
      }
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
    98
    val completion1 =
58853
f8715e7c1be6 discontinued obsolete control command category;
wenzelm
parents: 58753
diff changeset
    99
      if (replace == Some("")) completion
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   100
      else completion + (name, replace getOrElse name)
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   101
    new Outer_Syntax(keywords1, completion1, language_context, true)
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   102
  }
48706
e2b512024eab tuned signature;
wenzelm
parents: 48671
diff changeset
   103
48873
18b17f15bc62 more direct cumulation of (sparse) keywords;
wenzelm
parents: 48872
diff changeset
   104
  def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
18b17f15bc62 more direct cumulation of (sparse) keywords;
wenzelm
parents: 48872
diff changeset
   105
    (this /: keywords) {
58901
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
   106
      case (syntax, (name, opt_spec, replace)) =>
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
   107
        val opt_kind = opt_spec.map(_._1)
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   108
        syntax +
58901
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
   109
          (Symbol.decode(name), opt_kind, replace) +
47809a811eba clarified representation of type Keywords;
wenzelm
parents: 58900
diff changeset
   110
          (Symbol.encode(name), opt_kind, replace)
46940
a40be2f10ca9 explicit Outer_Syntax.Decl;
wenzelm
parents: 46712
diff changeset
   111
    }
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   112
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
   113
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   114
  /* merge */
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   115
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59073
diff changeset
   116
  def ++ (other: Prover.Syntax): Prover.Syntax =
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   117
    if (this eq other) this
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   118
    else {
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59073
diff changeset
   119
      val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59073
diff changeset
   120
      val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59073
diff changeset
   121
      if ((keywords eq keywords1) && (completion eq completion1)) this
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59073
diff changeset
   122
      else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   123
    }
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   124
dcecfcc56dce more merge operations;
wenzelm
parents: 58938
diff changeset
   125
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   126
  /* load commands */
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   127
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   128
  def load_command(name: String): Option[List[String]] = keywords.load_command(name)
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   129
  def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   130
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   131
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   132
  /* language context */
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   133
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   134
  def set_language_context(context: Completion.Language_Context): Outer_Syntax =
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   135
    new Outer_Syntax(keywords, completion, context, has_tokens)
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   136
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   137
  def no_tokens: Outer_Syntax =
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   138
  {
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58899
diff changeset
   139
    require(keywords.is_empty)
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   140
    new Outer_Syntax(
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   141
      completion = completion,
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   142
      language_context = language_context,
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   143
      has_tokens = false)
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   144
  }
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   145
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   146
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   147
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   148
  /** parsing **/
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   149
58697
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
   150
  /* line-oriented structure */
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   151
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   152
  def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   153
    : Outer_Syntax.Line_Structure =
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   154
  {
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   155
    val improper1 = tokens.forall(_.is_improper)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   156
    val command1 = tokens.exists(_.is_command)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   157
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   158
    val depth1 =
59122
c1dbcde94cd2 tuned signature;
wenzelm
parents: 59083
diff changeset
   159
      if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   160
      else if (command1) structure.after_span_depth
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   161
      else structure.span_depth
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   162
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   163
    val (span_depth1, after_span_depth1) =
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   164
      ((structure.span_depth, structure.after_span_depth) /: tokens) {
58703
883efcc7a50d more folds;
wenzelm
parents: 58700
diff changeset
   165
        case ((x, y), tok) =>
883efcc7a50d more folds;
wenzelm
parents: 58700
diff changeset
   166
          if (tok.is_command) {
60692
wenzelm
parents: 60215
diff changeset
   167
            if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
wenzelm
parents: 60215
diff changeset
   168
            else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
60694
b3fa4a8cdb5f clarified text folds: proof ... qed counts as extra block;
wenzelm
parents: 60692
diff changeset
   169
            else if (tok.is_command_kind(keywords, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
b3fa4a8cdb5f clarified text folds: proof ... qed counts as extra block;
wenzelm
parents: 60692
diff changeset
   170
            else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 3)
60692
wenzelm
parents: 60215
diff changeset
   171
            else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
wenzelm
parents: 60215
diff changeset
   172
            else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
wenzelm
parents: 60215
diff changeset
   173
            else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
58703
883efcc7a50d more folds;
wenzelm
parents: 58700
diff changeset
   174
            else (x, y)
883efcc7a50d more folds;
wenzelm
parents: 58700
diff changeset
   175
          }
883efcc7a50d more folds;
wenzelm
parents: 58700
diff changeset
   176
          else (x, y)
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   177
      }
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   178
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   179
    Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   180
  }
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   181
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   182
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   183
  /* command spans */
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   184
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   185
  def parse_spans(toks: List[Token]): List[Command_Span.Span] =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   186
  {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   187
    val result = new mutable.ListBuffer[Command_Span.Span]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   188
    val content = new mutable.ListBuffer[Token]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   189
    val improper = new mutable.ListBuffer[Token]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   190
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   191
    def ship(span: List[Token])
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   192
    {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   193
      val kind =
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   194
        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
   195
        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
   196
        else
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   197
          span.find(_.is_command) match {
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   198
            case None => Command_Span.Malformed_Span
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   199
            case Some(cmd) =>
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   200
              val name = cmd.source
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   201
              val offset =
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   202
                (0 /: span.takeWhile(_ != cmd)) {
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   203
                  case (i, tok) => i + Symbol.iterator(tok.source).length }
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   204
              val end_offset = offset + Symbol.iterator(name).length
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   205
              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
   206
              Command_Span.Command_Span(name, pos)
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   207
          }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   208
      result += Command_Span.Span(kind, span)
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   209
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   210
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   211
    def flush()
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   212
    {
59319
wenzelm
parents: 59122
diff changeset
   213
      if (content.nonEmpty) { ship(content.toList); content.clear }
wenzelm
parents: 59122
diff changeset
   214
      if (improper.nonEmpty) { ship(improper.toList); improper.clear }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   215
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   216
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   217
    for (tok <- toks) {
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   218
      if (tok.is_improper) improper += tok
59939
7d46aa03696e support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents: 59924
diff changeset
   219
      else if (tok.is_command_modifier ||
7d46aa03696e support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents: 59924
diff changeset
   220
        tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59735
diff changeset
   221
      { flush(); content += tok }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   222
      else { content ++= improper; improper.clear; content += tok }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   223
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   224
    flush()
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   225
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   226
    result.toList
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   227
  }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   228
57906
020df63dd0a9 tuned signature;
wenzelm
parents: 57905
diff changeset
   229
  def parse_spans(input: CharSequence): List[Command_Span.Span] =
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59077
diff changeset
   230
    parse_spans(Token.explode(keywords, input))
57906
020df63dd0a9 tuned signature;
wenzelm
parents: 57905
diff changeset
   231
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   232
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   233
  /* overall document structure */
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   234
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   235
  def heading_level(command: Command): Option[Int] =
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   236
  {
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   237
    val name = command.span.name
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   238
    name match {
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   239
      case Thy_Header.CHAPTER => Some(0)
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   240
      case Thy_Header.SECTION | Thy_Header.HEADER => Some(1)
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   241
      case Thy_Header.SUBSECTION => Some(2)
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   242
      case Thy_Header.SUBSUBSECTION => Some(3)
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   243
      case _ =>
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   244
        keywords.command_kind(name) match {
59700
d887abcc7c24 more command categories, as in ML;
wenzelm
parents: 59684
diff changeset
   245
          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   246
          case _ => None
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   247
        }
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   248
    }
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   249
  }
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   250
58743
c07a59140fee clarified tree root;
wenzelm
parents: 58706
diff changeset
   251
  def parse_document(node_name: Document.Node.Name, text: CharSequence):
c07a59140fee clarified tree root;
wenzelm
parents: 58706
diff changeset
   252
    List[Outer_Syntax.Document] =
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   253
  {
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   254
    /* stack operations */
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   255
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   256
    def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   257
      new mutable.ListBuffer[Outer_Syntax.Document]
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   258
58747
c680f181b32e tuned rendering;
wenzelm
parents: 58743
diff changeset
   259
    var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
c680f181b32e tuned rendering;
wenzelm
parents: 58743
diff changeset
   260
      List((0, Command.empty, buffer()))
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   261
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   262
    @tailrec def close(level: Int => Boolean)
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   263
    {
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   264
      stack match {
58747
c680f181b32e tuned rendering;
wenzelm
parents: 58743
diff changeset
   265
        case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59702
diff changeset
   266
          body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   267
          stack = stack.tail
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   268
          close(level)
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   269
        case _ =>
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   270
      }
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   271
    }
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   272
58743
c07a59140fee clarified tree root;
wenzelm
parents: 58706
diff changeset
   273
    def result(): List[Outer_Syntax.Document] =
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   274
    {
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   275
      close(_ => true)
58743
c07a59140fee clarified tree root;
wenzelm
parents: 58706
diff changeset
   276
      stack.head._3.toList
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   277
    }
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   278
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   279
    def add(command: Command)
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   280
    {
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   281
      heading_level(command) match {
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   282
        case Some(i) =>
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   283
          close(_ > i)
58747
c680f181b32e tuned rendering;
wenzelm
parents: 58743
diff changeset
   284
          stack = (i + 1, command, buffer()) :: stack
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   285
        case None =>
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   286
      }
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   287
      stack.head._3 += Outer_Syntax.Document_Atom(command)
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   288
    }
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   289
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   290
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   291
    /* result structure */
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   292
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   293
    val spans = parse_spans(text)
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59700
diff changeset
   294
    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
58706
70a947611792 tuned signature and modules;
wenzelm
parents: 58703
diff changeset
   295
    result()
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   296
  }
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   297
}