src/Pure/Isar/outer_syntax.scala
author wenzelm
Sat, 18 Oct 2014 20:56:16 +0200
changeset 58700 4717d18cc619
parent 58697 5bc1d6c4a499
child 58703 883efcc7a50d
permissions -rw-r--r--
clarified Line_Structure wrt. command span;
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
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    10
import scala.util.parsing.input.{Reader, CharSequenceReader}
43411
0206466ee473 some support for partial scans with explicit context;
wenzelm
parents: 40533
diff changeset
    11
import scala.collection.mutable
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
{
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    16
  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
    17
  {
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    18
    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
    19
    result += '"'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    20
    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
    21
      if (s.length == 1) {
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    22
        val c = s(0)
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    23
        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
    24
          result += '\\'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    25
          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
    26
          if (c < 100) result += '0'
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    27
          result ++= (c.asInstanceOf[Int].toString)
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    28
        }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    29
        else result += c
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    30
      }
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    31
      else result ++= s
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    32
    }
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
    result.toString
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    35
  }
46626
a02115865bcc streamlined abstract datatype;
wenzelm
parents: 46624
diff changeset
    36
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46940
diff changeset
    37
  val empty: Outer_Syntax = new Outer_Syntax()
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48864
diff changeset
    38
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46940
diff changeset
    39
  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    40
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    41
58697
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
    42
  /* line-oriented structure */
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    43
58697
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
    44
  object Line_Structure
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    45
  {
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    46
    val init = Line_Structure()
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    47
  }
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    48
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    49
  sealed case class Line_Structure(
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    50
    improper: Boolean = true,
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    51
    command: Boolean = false,
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    52
    depth: Int = 0,
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    53
    span_depth: Int = 0,
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
    54
    after_span_depth: Int = 0)
43774
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    55
}
6dfdb70496fe added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents: 43695
diff changeset
    56
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46626
diff changeset
    57
final class Outer_Syntax private(
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48708
diff changeset
    58
  keywords: Map[String, (String, List[String])] = Map.empty,
46626
a02115865bcc streamlined abstract datatype;
wenzelm
parents: 46624
diff changeset
    59
  lexicon: Scan.Lexicon = Scan.Lexicon.empty,
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
    60
  val completion: Completion = Completion.empty,
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
    61
  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
    62
  val has_tokens: Boolean = true) extends Prover.Syntax
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    63
{
48660
730ca503e955 static outer syntax based on session specifications;
wenzelm
parents: 47469
diff changeset
    64
  override def toString: String =
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48708
diff changeset
    65
    (for ((name, (kind, files)) <- keywords) yield {
48660
730ca503e955 static outer syntax based on session specifications;
wenzelm
parents: 47469
diff changeset
    66
      if (kind == Keyword.MINOR) quote(name)
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48708
diff changeset
    67
      else
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48708
diff changeset
    68
        quote(name) + " :: " + quote(kind) +
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48708
diff changeset
    69
        (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
48671
951bc4c3ee17 refined outer syntax;
wenzelm
parents: 48660
diff changeset
    70
    }).toList.sorted.mkString("keywords\n  ", " and\n  ", "")
48660
730ca503e955 static outer syntax based on session specifications;
wenzelm
parents: 47469
diff changeset
    71
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    72
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    73
  /* keyword kind */
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    74
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48708
diff changeset
    75
  def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48708
diff changeset
    76
  def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
38471
0924654b8163 report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
wenzelm
parents: 36956
diff changeset
    77
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    78
  def is_command(name: String): Boolean =
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    79
    keyword_kind(name) match {
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    80
      case Some(kind) => kind != Keyword.MINOR
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    81
      case None => false
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    82
    }
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    83
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    84
  def command_kind(token: Token, pred: String => Boolean): Boolean =
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    85
    token.is_command && is_command(token.source) &&
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    86
      pred(keyword_kind(token.source).get)
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
    87
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    88
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    89
  /* load commands */
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
    90
57901
e1abca2527da more explicit type Span in Scala, according to ML version;
wenzelm
parents: 56393
diff changeset
    91
  def load_command(name: String): Option[List[String]] =
e1abca2527da more explicit type Span in Scala, according to ML version;
wenzelm
parents: 56393
diff changeset
    92
    keywords.get(name) match {
54513
5545aff878b1 inline blobs into command, via SHA1 digest;
wenzelm
parents: 54462
diff changeset
    93
      case Some((Keyword.THY_LOAD, exts)) => Some(exts)
54462
c9bb76303348 explicit indication of thy_load commands;
wenzelm
parents: 53280
diff changeset
    94
      case _ => None
c9bb76303348 explicit indication of thy_load commands;
wenzelm
parents: 53280
diff changeset
    95
    }
c9bb76303348 explicit indication of thy_load commands;
wenzelm
parents: 53280
diff changeset
    96
56314
9a513737a0b2 tuned signature;
wenzelm
parents: 55749
diff changeset
    97
  val load_commands: List[(String, List[String])] =
48885
d5fdaf7dd1f8 find files via load commands within theory text;
wenzelm
parents: 48873
diff changeset
    98
    (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
48872
6124e0d1120a some support for thy_load_commands;
wenzelm
parents: 48870
diff changeset
    99
56393
22f533e6a049 more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents: 56314
diff changeset
   100
  def load_commands_in(text: String): Boolean =
22f533e6a049 more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents: 56314
diff changeset
   101
    load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
22f533e6a049 more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents: 56314
diff changeset
   102
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
   103
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
   104
  /* add keywords */
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
   105
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   106
  def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   107
  {
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   108
    val keywords1 = keywords + (name -> kind)
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   109
    val lexicon1 = lexicon + name
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   110
    val completion1 =
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   111
      if (Keyword.control(kind._1) || replace == Some("")) completion
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   112
      else completion + (name, replace getOrElse name)
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
   113
    new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true)
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   114
  }
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   115
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   116
  def + (name: String, kind: (String, List[String])): Outer_Syntax =
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   117
    this + (name, kind, Some(name))
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   118
  def + (name: String, kind: String): Outer_Syntax =
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   119
    this + (name, (kind, Nil), Some(name))
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   120
  def + (name: String, replace: Option[String]): Outer_Syntax =
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   121
    this + (name, (Keyword.MINOR, Nil), replace)
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   122
  def + (name: String): Outer_Syntax = this + (name, None)
48706
e2b512024eab tuned signature;
wenzelm
parents: 48671
diff changeset
   123
48873
18b17f15bc62 more direct cumulation of (sparse) keywords;
wenzelm
parents: 48872
diff changeset
   124
  def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
18b17f15bc62 more direct cumulation of (sparse) keywords;
wenzelm
parents: 48872
diff changeset
   125
    (this /: keywords) {
52439
4cf3f6153eb8 improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents: 52066
diff changeset
   126
      case (syntax, (name, Some((kind, _)), replace)) =>
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   127
        syntax +
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   128
          (Symbol.decode(name), kind, replace) +
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   129
          (Symbol.encode(name), kind, replace)
52439
4cf3f6153eb8 improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents: 52066
diff changeset
   130
      case (syntax, (name, None, replace)) =>
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   131
        syntax +
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   132
          (Symbol.decode(name), replace) +
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48885
diff changeset
   133
          (Symbol.encode(name), replace)
46940
a40be2f10ca9 explicit Outer_Syntax.Decl;
wenzelm
parents: 46712
diff changeset
   134
    }
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   135
58695
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
   136
91839729224e tuned comments;
wenzelm
parents: 58694
diff changeset
   137
  /* document headings */
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   138
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   139
  def heading_level(name: String): Option[Int] =
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   140
  {
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   141
    keyword_kind(name) match {
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   142
      case _ if name == "header" => Some(0)
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   143
      case Some(Keyword.THY_HEADING1) => Some(1)
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   144
      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   145
      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   146
      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   147
      case Some(kind) if Keyword.theory(kind) => Some(5)
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   148
      case _ => None
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   149
    }
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46941
diff changeset
   150
  }
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   151
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   152
  def heading_level(command: Command): Option[Int] =
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   153
    heading_level(command.name)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38471
diff changeset
   154
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   155
58697
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
   156
  /* line-oriented structure */
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   157
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   158
  def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   159
    : Outer_Syntax.Line_Structure =
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   160
  {
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   161
    val improper1 = tokens.forall(_.is_improper)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   162
    val command1 = tokens.exists(_.is_command)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   163
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   164
    val depth1 =
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   165
      if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   166
      else if (command1) struct.after_span_depth
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   167
      else struct.span_depth
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   168
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   169
    val (span_depth1, after_span_depth1) =
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   170
      ((struct.span_depth, struct.after_span_depth) /: tokens) {
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   171
        case ((d0, d), tok) =>
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   172
          if (command_kind(tok, Keyword.theory_goal)) (2, 1)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   173
          else if (command_kind(tok, Keyword.theory)) (1, 0)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   174
          else if (command_kind(tok, Keyword.proof_goal)) (d + 2, d + 1)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   175
          else if (command_kind(tok, Keyword.qed)) (d + 1, d - 1)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   176
          else if (command_kind(tok, Keyword.qed_global)) (1, 0)
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   177
          else (d0, d)
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   178
      }
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   179
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   180
    Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   181
  }
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   182
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   183
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   184
  /* token language */
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 52439
diff changeset
   185
57907
7fc36b4c7cce tuned signature;
wenzelm
parents: 57906
diff changeset
   186
  def scan(input: CharSequence): List[Token] =
52066
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   187
  {
58503
wenzelm
parents: 57911
diff changeset
   188
    val in: Reader[Char] = new CharSequenceReader(input)
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   189
    Token.Parsers.parseAll(
57907
7fc36b4c7cce tuned signature;
wenzelm
parents: 57906
diff changeset
   190
        Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), in) match {
55494
009b71c1ed23 tuned signature (in accordance to ML version);
wenzelm
parents: 55492
diff changeset
   191
      case Token.Parsers.Success(tokens, _) => tokens
57907
7fc36b4c7cce tuned signature;
wenzelm
parents: 57906
diff changeset
   192
      case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   193
    }
52066
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   194
  }
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   195
58697
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
   196
  def scan_line(
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
   197
    input: CharSequence,
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
   198
    context: Scan.Line_Context,
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
   199
    structure: Outer_Syntax.Line_Structure)
5bc1d6c4a499 tuned signature;
wenzelm
parents: 58696
diff changeset
   200
    : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Structure) =
52066
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   201
  {
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   202
    var in: Reader[Char] = new CharSequenceReader(input)
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   203
    val toks = new mutable.ListBuffer[Token]
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   204
    var ctxt = context
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   205
    while (!in.atEnd) {
55510
1585a65aad64 tuned signature -- emphasize line-oriented aspect;
wenzelm
parents: 55494
diff changeset
   206
      Token.Parsers.parse(Token.Parsers.token_line(lexicon, is_command, ctxt), in) match {
55494
009b71c1ed23 tuned signature (in accordance to ML version);
wenzelm
parents: 55492
diff changeset
   207
        case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
009b71c1ed23 tuned signature (in accordance to ML version);
wenzelm
parents: 55492
diff changeset
   208
        case Token.Parsers.NoSuccess(_, rest) =>
52066
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   209
          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
43411
0206466ee473 some support for partial scans with explicit context;
wenzelm
parents: 40533
diff changeset
   210
      }
0206466ee473 some support for partial scans with explicit context;
wenzelm
parents: 40533
diff changeset
   211
    }
58696
6b7445774ce3 more explicit Line_Nesting;
wenzelm
parents: 58695
diff changeset
   212
    val tokens = toks.toList
58700
4717d18cc619 clarified Line_Structure wrt. command span;
wenzelm
parents: 58697
diff changeset
   213
    (tokens, ctxt, line_structure(tokens, structure))
52066
83b7b88770c9 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50428
diff changeset
   214
  }
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   215
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   216
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   217
  /* parse_spans */
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   218
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   219
  def parse_spans(toks: List[Token]): List[Command_Span.Span] =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   220
  {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   221
    val result = new mutable.ListBuffer[Command_Span.Span]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   222
    val content = new mutable.ListBuffer[Token]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   223
    val improper = new mutable.ListBuffer[Token]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   224
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   225
    def ship(span: List[Token])
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   226
    {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   227
      val kind =
57910
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57907
diff changeset
   228
        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57907
diff changeset
   229
          val name = span.head.source
57911
dcb758188aa6 clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents: 57910
diff changeset
   230
          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
57910
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57907
diff changeset
   231
          Command_Span.Command_Span(name, pos)
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57907
diff changeset
   232
        }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   233
        else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   234
        else Command_Span.Malformed_Span
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   235
      result += Command_Span.Span(kind, span)
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   236
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   237
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   238
    def flush()
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   239
    {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   240
      if (!content.isEmpty) { ship(content.toList); content.clear }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   241
      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   242
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   243
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   244
    for (tok <- toks) {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   245
      if (tok.is_command) { flush(); content += tok }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   246
      else if (tok.is_improper) improper += tok
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   247
      else { content ++= improper; improper.clear; content += tok }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   248
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   249
    flush()
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   250
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   251
    result.toList
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   252
  }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   253
57906
020df63dd0a9 tuned signature;
wenzelm
parents: 57905
diff changeset
   254
  def parse_spans(input: CharSequence): List[Command_Span.Span] =
020df63dd0a9 tuned signature;
wenzelm
parents: 57905
diff changeset
   255
    parse_spans(scan(input))
020df63dd0a9 tuned signature;
wenzelm
parents: 57905
diff changeset
   256
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57901
diff changeset
   257
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   258
  /* language context */
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   259
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
   260
  def set_language_context(context: Completion.Language_Context): Outer_Syntax =
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   261
    new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   262
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   263
  def no_tokens: Outer_Syntax =
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   264
  {
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   265
    require(keywords.isEmpty && lexicon.isEmpty)
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   266
    new Outer_Syntax(
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   267
      completion = completion,
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
   268
      language_context = language_context,
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   269
      has_tokens = false)
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55510
diff changeset
   270
  }
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
   271
}