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