src/Pure/Isar/outer_syntax.scala
author wenzelm
Thu Oct 16 21:24:42 2014 +0200 (2014-10-16)
changeset 58696 6b7445774ce3
parent 58695 91839729224e
child 58697 5bc1d6c4a499
permissions -rw-r--r--
more explicit Line_Nesting;
wenzelm@34166
     1
/*  Title:      Pure/Isar/outer_syntax.scala
wenzelm@34166
     2
    Author:     Makarius
wenzelm@34166
     3
wenzelm@34166
     4
Isabelle/Isar outer syntax.
wenzelm@34166
     5
*/
wenzelm@34166
     6
wenzelm@34166
     7
package isabelle
wenzelm@34166
     8
wenzelm@34166
     9
wenzelm@34166
    10
import scala.util.parsing.input.{Reader, CharSequenceReader}
wenzelm@43411
    11
import scala.collection.mutable
wenzelm@34166
    12
wenzelm@34166
    13
wenzelm@43774
    14
object Outer_Syntax
wenzelm@43774
    15
{
wenzelm@43774
    16
  def quote_string(str: String): String =
wenzelm@43774
    17
  {
wenzelm@43774
    18
    val result = new StringBuilder(str.length + 10)
wenzelm@43774
    19
    result += '"'
wenzelm@43774
    20
    for (s <- Symbol.iterator(str)) {
wenzelm@43774
    21
      if (s.length == 1) {
wenzelm@43774
    22
        val c = s(0)
wenzelm@43774
    23
        if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
wenzelm@43774
    24
          result += '\\'
wenzelm@43774
    25
          if (c < 10) result += '0'
wenzelm@43774
    26
          if (c < 100) result += '0'
wenzelm@43774
    27
          result ++= (c.asInstanceOf[Int].toString)
wenzelm@43774
    28
        }
wenzelm@43774
    29
        else result += c
wenzelm@43774
    30
      }
wenzelm@43774
    31
      else result ++= s
wenzelm@43774
    32
    }
wenzelm@43774
    33
    result += '"'
wenzelm@43774
    34
    result.toString
wenzelm@43774
    35
  }
wenzelm@46626
    36
wenzelm@46941
    37
  val empty: Outer_Syntax = new Outer_Syntax()
wenzelm@48870
    38
wenzelm@46941
    39
  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
wenzelm@58696
    40
wenzelm@58696
    41
wenzelm@58696
    42
  /* line nesting */
wenzelm@58696
    43
wenzelm@58696
    44
  object Line_Nesting
wenzelm@58696
    45
  {
wenzelm@58696
    46
    val init = Line_Nesting(0, 0)
wenzelm@58696
    47
  }
wenzelm@58696
    48
wenzelm@58696
    49
  sealed case class Line_Nesting(depth_before: Int, depth: Int)
wenzelm@43774
    50
}
wenzelm@43774
    51
wenzelm@46712
    52
final class Outer_Syntax private(
wenzelm@48864
    53
  keywords: Map[String, (String, List[String])] = Map.empty,
wenzelm@46626
    54
  lexicon: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@53280
    55
  val completion: Completion = Completion.empty,
wenzelm@55749
    56
  val language_context: Completion.Language_Context = Completion.Language_Context.outer,
wenzelm@56393
    57
  val has_tokens: Boolean = true) extends Prover.Syntax
wenzelm@34166
    58
{
wenzelm@48660
    59
  override def toString: String =
wenzelm@48864
    60
    (for ((name, (kind, files)) <- keywords) yield {
wenzelm@48660
    61
      if (kind == Keyword.MINOR) quote(name)
wenzelm@48864
    62
      else
wenzelm@48864
    63
        quote(name) + " :: " + quote(kind) +
wenzelm@48864
    64
        (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
wenzelm@48671
    65
    }).toList.sorted.mkString("keywords\n  ", " and\n  ", "")
wenzelm@48660
    66
wenzelm@58695
    67
wenzelm@58695
    68
  /* keyword kind */
wenzelm@58695
    69
wenzelm@48864
    70
  def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
wenzelm@48864
    71
  def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
wenzelm@38471
    72
wenzelm@58695
    73
  def is_command(name: String): Boolean =
wenzelm@58695
    74
    keyword_kind(name) match {
wenzelm@58695
    75
      case Some(kind) => kind != Keyword.MINOR
wenzelm@58695
    76
      case None => false
wenzelm@58695
    77
    }
wenzelm@58695
    78
wenzelm@58696
    79
  def command_kind(token: Token, pred: String => Boolean): Boolean =
wenzelm@58696
    80
    token.is_command && is_command(token.source) &&
wenzelm@58696
    81
      pred(keyword_kind(token.source).get)
wenzelm@58696
    82
wenzelm@58695
    83
wenzelm@58695
    84
  /* load commands */
wenzelm@58695
    85
wenzelm@57901
    86
  def load_command(name: String): Option[List[String]] =
wenzelm@57901
    87
    keywords.get(name) match {
wenzelm@54513
    88
      case Some((Keyword.THY_LOAD, exts)) => Some(exts)
wenzelm@54462
    89
      case _ => None
wenzelm@54462
    90
    }
wenzelm@54462
    91
wenzelm@56314
    92
  val load_commands: List[(String, List[String])] =
wenzelm@48885
    93
    (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
wenzelm@48872
    94
wenzelm@56393
    95
  def load_commands_in(text: String): Boolean =
wenzelm@56393
    96
    load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
wenzelm@56393
    97
wenzelm@58695
    98
wenzelm@58695
    99
  /* add keywords */
wenzelm@58695
   100
wenzelm@50128
   101
  def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
wenzelm@53280
   102
  {
wenzelm@53280
   103
    val keywords1 = keywords + (name -> kind)
wenzelm@53280
   104
    val lexicon1 = lexicon + name
wenzelm@53280
   105
    val completion1 =
wenzelm@50128
   106
      if (Keyword.control(kind._1) || replace == Some("")) completion
wenzelm@53280
   107
      else completion + (name, replace getOrElse name)
wenzelm@55749
   108
    new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true)
wenzelm@53280
   109
  }
wenzelm@34166
   110
wenzelm@53280
   111
  def + (name: String, kind: (String, List[String])): Outer_Syntax =
wenzelm@53280
   112
    this + (name, kind, Some(name))
wenzelm@53280
   113
  def + (name: String, kind: String): Outer_Syntax =
wenzelm@53280
   114
    this + (name, (kind, Nil), Some(name))
wenzelm@50128
   115
  def + (name: String, replace: Option[String]): Outer_Syntax =
wenzelm@50128
   116
    this + (name, (Keyword.MINOR, Nil), replace)
wenzelm@50128
   117
  def + (name: String): Outer_Syntax = this + (name, None)
wenzelm@48706
   118
wenzelm@48873
   119
  def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
wenzelm@48873
   120
    (this /: keywords) {
wenzelm@52439
   121
      case (syntax, (name, Some((kind, _)), replace)) =>
wenzelm@50128
   122
        syntax +
wenzelm@50128
   123
          (Symbol.decode(name), kind, replace) +
wenzelm@50128
   124
          (Symbol.encode(name), kind, replace)
wenzelm@52439
   125
      case (syntax, (name, None, replace)) =>
wenzelm@50128
   126
        syntax +
wenzelm@50128
   127
          (Symbol.decode(name), replace) +
wenzelm@50128
   128
          (Symbol.encode(name), replace)
wenzelm@46940
   129
    }
wenzelm@34166
   130
wenzelm@58695
   131
wenzelm@58695
   132
  /* document headings */
wenzelm@34166
   133
wenzelm@40454
   134
  def heading_level(name: String): Option[Int] =
wenzelm@46969
   135
  {
wenzelm@46969
   136
    keyword_kind(name) match {
wenzelm@46969
   137
      case _ if name == "header" => Some(0)
wenzelm@46969
   138
      case Some(Keyword.THY_HEADING1) => Some(1)
wenzelm@46969
   139
      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
wenzelm@46969
   140
      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
wenzelm@46969
   141
      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
wenzelm@46969
   142
      case Some(kind) if Keyword.theory(kind) => Some(5)
wenzelm@46969
   143
      case _ => None
wenzelm@40454
   144
    }
wenzelm@46969
   145
  }
wenzelm@40454
   146
wenzelm@40454
   147
  def heading_level(command: Command): Option[Int] =
wenzelm@40454
   148
    heading_level(command.name)
wenzelm@40454
   149
wenzelm@34166
   150
wenzelm@58696
   151
  /* line nesting */
wenzelm@58696
   152
wenzelm@58696
   153
  def line_nesting(tokens: List[Token], depth: Int): Outer_Syntax.Line_Nesting =
wenzelm@58696
   154
  {
wenzelm@58696
   155
    val depth1 =
wenzelm@58696
   156
      if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
wenzelm@58696
   157
      else depth
wenzelm@58696
   158
    val depth2 =
wenzelm@58696
   159
      (depth /: tokens) { case (d, tok) =>
wenzelm@58696
   160
        if (command_kind(tok, Keyword.theory_goal)) 1
wenzelm@58696
   161
        else if (command_kind(tok, Keyword.theory)) 0
wenzelm@58696
   162
        else if (command_kind(tok, Keyword.proof_goal)) d + 1
wenzelm@58696
   163
        else if (command_kind(tok, Keyword.qed)) d - 1
wenzelm@58696
   164
        else if (command_kind(tok, Keyword.qed_global)) 0
wenzelm@58696
   165
        else d
wenzelm@58696
   166
      }
wenzelm@58696
   167
    Outer_Syntax.Line_Nesting(depth1, depth2)
wenzelm@58696
   168
  }
wenzelm@58696
   169
wenzelm@58696
   170
wenzelm@53280
   171
  /* token language */
wenzelm@53280
   172
wenzelm@57907
   173
  def scan(input: CharSequence): List[Token] =
wenzelm@52066
   174
  {
wenzelm@58503
   175
    val in: Reader[Char] = new CharSequenceReader(input)
wenzelm@55616
   176
    Token.Parsers.parseAll(
wenzelm@57907
   177
        Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), in) match {
wenzelm@55494
   178
      case Token.Parsers.Success(tokens, _) => tokens
wenzelm@57907
   179
      case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
wenzelm@34166
   180
    }
wenzelm@52066
   181
  }
wenzelm@34166
   182
wenzelm@58696
   183
  def scan_line(input: CharSequence, context: Scan.Line_Context, nesting: Outer_Syntax.Line_Nesting)
wenzelm@58696
   184
    : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Nesting) =
wenzelm@52066
   185
  {
wenzelm@52066
   186
    var in: Reader[Char] = new CharSequenceReader(input)
wenzelm@52066
   187
    val toks = new mutable.ListBuffer[Token]
wenzelm@52066
   188
    var ctxt = context
wenzelm@52066
   189
    while (!in.atEnd) {
wenzelm@55510
   190
      Token.Parsers.parse(Token.Parsers.token_line(lexicon, is_command, ctxt), in) match {
wenzelm@55494
   191
        case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
wenzelm@55494
   192
        case Token.Parsers.NoSuccess(_, rest) =>
wenzelm@52066
   193
          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
wenzelm@43411
   194
      }
wenzelm@43411
   195
    }
wenzelm@58696
   196
    val tokens = toks.toList
wenzelm@58696
   197
    (tokens, ctxt, line_nesting(tokens, nesting.depth))
wenzelm@52066
   198
  }
wenzelm@55616
   199
wenzelm@55616
   200
wenzelm@57905
   201
  /* parse_spans */
wenzelm@57905
   202
wenzelm@57905
   203
  def parse_spans(toks: List[Token]): List[Command_Span.Span] =
wenzelm@57905
   204
  {
wenzelm@57905
   205
    val result = new mutable.ListBuffer[Command_Span.Span]
wenzelm@57905
   206
    val content = new mutable.ListBuffer[Token]
wenzelm@57905
   207
    val improper = new mutable.ListBuffer[Token]
wenzelm@57905
   208
wenzelm@57905
   209
    def ship(span: List[Token])
wenzelm@57905
   210
    {
wenzelm@57905
   211
      val kind =
wenzelm@57910
   212
        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
wenzelm@57910
   213
          val name = span.head.source
wenzelm@57911
   214
          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
wenzelm@57910
   215
          Command_Span.Command_Span(name, pos)
wenzelm@57910
   216
        }
wenzelm@57905
   217
        else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
wenzelm@57905
   218
        else Command_Span.Malformed_Span
wenzelm@57905
   219
      result += Command_Span.Span(kind, span)
wenzelm@57905
   220
    }
wenzelm@57905
   221
wenzelm@57905
   222
    def flush()
wenzelm@57905
   223
    {
wenzelm@57905
   224
      if (!content.isEmpty) { ship(content.toList); content.clear }
wenzelm@57905
   225
      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
wenzelm@57905
   226
    }
wenzelm@57905
   227
wenzelm@57905
   228
    for (tok <- toks) {
wenzelm@57905
   229
      if (tok.is_command) { flush(); content += tok }
wenzelm@57905
   230
      else if (tok.is_improper) improper += tok
wenzelm@57905
   231
      else { content ++= improper; improper.clear; content += tok }
wenzelm@57905
   232
    }
wenzelm@57905
   233
    flush()
wenzelm@57905
   234
wenzelm@57905
   235
    result.toList
wenzelm@57905
   236
  }
wenzelm@57905
   237
wenzelm@57906
   238
  def parse_spans(input: CharSequence): List[Command_Span.Span] =
wenzelm@57906
   239
    parse_spans(scan(input))
wenzelm@57906
   240
wenzelm@57905
   241
wenzelm@55616
   242
  /* language context */
wenzelm@55616
   243
wenzelm@55749
   244
  def set_language_context(context: Completion.Language_Context): Outer_Syntax =
wenzelm@55616
   245
    new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
wenzelm@55616
   246
wenzelm@55616
   247
  def no_tokens: Outer_Syntax =
wenzelm@55616
   248
  {
wenzelm@55616
   249
    require(keywords.isEmpty && lexicon.isEmpty)
wenzelm@55616
   250
    new Outer_Syntax(
wenzelm@55616
   251
      completion = completion,
wenzelm@55749
   252
      language_context = language_context,
wenzelm@55616
   253
      has_tokens = false)
wenzelm@55616
   254
  }
wenzelm@34166
   255
}