src/Pure/Isar/outer_syntax.scala
author wenzelm
Wed Sep 14 12:56:57 2016 +0200 (2016-09-14)
changeset 63867 fb46c031c841
parent 63865 ccac33e291b1
child 64616 dc3ec40fe41b
permissions -rw-r--r--
maintain abbrevs in canonical reverse order;
     1 /*  Title:      Pure/Isar/outer_syntax.scala
     2     Author:     Makarius
     3 
     4 Isabelle/Isar outer syntax.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.mutable
    11 
    12 
    13 object Outer_Syntax
    14 {
    15   /* syntax */
    16 
    17   val empty: Outer_Syntax = new Outer_Syntax()
    18 
    19   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
    20 
    21 
    22   /* string literals */
    23 
    24   def quote_string(str: String): String =
    25   {
    26     val result = new StringBuilder(str.length + 10)
    27     result += '"'
    28     for (s <- Symbol.iterator(str)) {
    29       if (s.length == 1) {
    30         val c = s(0)
    31         if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
    32           result += '\\'
    33           if (c < 10) result += '0'
    34           if (c < 100) result += '0'
    35           result ++= c.asInstanceOf[Int].toString
    36         }
    37         else result += c
    38       }
    39       else result ++= s
    40     }
    41     result += '"'
    42     result.toString
    43   }
    44 }
    45 
    46 final class Outer_Syntax private(
    47   val keywords: Keyword.Keywords = Keyword.Keywords.empty,
    48   val completion: Completion = Completion.empty,
    49   val rev_abbrevs: Thy_Header.Abbrevs = Nil,
    50   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
    51   val has_tokens: Boolean = true)
    52 {
    53   /** syntax content **/
    54 
    55   override def toString: String = keywords.toString
    56 
    57 
    58   /* keywords */
    59 
    60   def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
    61   {
    62     val keywords1 = keywords + (name, kind, tags)
    63     val completion1 =
    64       completion.add_keyword(name).
    65         add_abbrevs(
    66           (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
    67            else Nil) :::
    68           (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
    69     new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
    70   }
    71 
    72   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    73     (this /: keywords) {
    74       case (syntax, (name, ((kind, tags), _))) =>
    75         syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
    76     }
    77 
    78 
    79   /* abbrevs */
    80 
    81   def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse
    82 
    83   def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
    84     if (new_abbrevs.isEmpty) this
    85     else {
    86       val completion1 =
    87         completion.add_abbrevs(
    88           (for ((a, b) <- new_abbrevs) yield {
    89             val a1 = Symbol.decode(a)
    90             val a2 = Symbol.encode(a)
    91             val b1 = Symbol.decode(b)
    92             List((a1, b1), (a2, b1))
    93           }).flatten)
    94       val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
    95       new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens)
    96     }
    97 
    98 
    99   /* merge */
   100 
   101   def ++ (other: Outer_Syntax): Outer_Syntax =
   102     if (this eq other) this
   103     else {
   104       val keywords1 = keywords ++ other.keywords
   105       val completion1 = completion ++ other.completion
   106       val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
   107       if ((keywords eq keywords1) && (completion eq completion1)) this
   108       else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
   109     }
   110 
   111 
   112   /* load commands */
   113 
   114   def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
   115   def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
   116 
   117 
   118   /* language context */
   119 
   120   def set_language_context(context: Completion.Language_Context): Outer_Syntax =
   121     new Outer_Syntax(keywords, completion, rev_abbrevs, context, has_tokens)
   122 
   123   def no_tokens: Outer_Syntax =
   124   {
   125     require(keywords.is_empty)
   126     new Outer_Syntax(
   127       completion = completion,
   128       rev_abbrevs = rev_abbrevs,
   129       language_context = language_context,
   130       has_tokens = false)
   131   }
   132 
   133 
   134 
   135   /** parsing **/
   136 
   137   /* command spans */
   138 
   139   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   140   {
   141     val result = new mutable.ListBuffer[Command_Span.Span]
   142     val content = new mutable.ListBuffer[Token]
   143     val improper = new mutable.ListBuffer[Token]
   144 
   145     def ship(span: List[Token])
   146     {
   147       val kind =
   148         if (span.forall(_.is_improper)) Command_Span.Ignored_Span
   149         else if (span.exists(_.is_error)) Command_Span.Malformed_Span
   150         else
   151           span.find(_.is_command) match {
   152             case None => Command_Span.Malformed_Span
   153             case Some(cmd) =>
   154               val name = cmd.source
   155               val offset =
   156                 (0 /: span.takeWhile(_ != cmd)) {
   157                   case (i, tok) => i + Symbol.iterator(tok.source).length }
   158               val end_offset = offset + Symbol.iterator(name).length
   159               val pos = Position.Range(Text.Range(offset, end_offset) + 1)
   160               Command_Span.Command_Span(name, pos)
   161           }
   162       result += Command_Span.Span(kind, span)
   163     }
   164 
   165     def flush()
   166     {
   167       if (content.nonEmpty) { ship(content.toList); content.clear }
   168       if (improper.nonEmpty) { ship(improper.toList); improper.clear }
   169     }
   170 
   171     for (tok <- toks) {
   172       if (tok.is_improper) improper += tok
   173       else if (keywords.is_before_command(tok) ||
   174         tok.is_command &&
   175           (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
   176       { flush(); content += tok }
   177       else { content ++= improper; improper.clear; content += tok }
   178     }
   179     flush()
   180 
   181     result.toList
   182   }
   183 
   184   def parse_spans(input: CharSequence): List[Command_Span.Span] =
   185     parse_spans(Token.explode(keywords, input))
   186 }