src/Pure/Isar/outer_syntax.scala
author wenzelm
Thu Aug 04 10:55:51 2016 +0200 (2016-08-04)
changeset 63603 9d9ea2c6bc38
parent 63592 64db21931bcb
child 63604 d8de4f8b95eb
permissions -rw-r--r--
clarified modules;
     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 import scala.annotation.tailrec
    12 
    13 
    14 object Outer_Syntax
    15 {
    16   /* syntax */
    17 
    18   val empty: Outer_Syntax = new Outer_Syntax()
    19 
    20   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
    21 
    22 
    23   /* string literals */
    24 
    25   def quote_string(str: String): String =
    26   {
    27     val result = new StringBuilder(str.length + 10)
    28     result += '"'
    29     for (s <- Symbol.iterator(str)) {
    30       if (s.length == 1) {
    31         val c = s(0)
    32         if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
    33           result += '\\'
    34           if (c < 10) result += '0'
    35           if (c < 100) result += '0'
    36           result ++= c.asInstanceOf[Int].toString
    37         }
    38         else result += c
    39       }
    40       else result ++= s
    41     }
    42     result += '"'
    43     result.toString
    44   }
    45 
    46 
    47   /* overall document structure */
    48 
    49   sealed abstract class Document { def length: Int }
    50   case class Document_Block(name: String, text: String, body: List[Document]) extends Document
    51   {
    52     val length: Int = (0 /: body)(_ + _.length)
    53   }
    54   case class Document_Atom(command: Command) extends Document
    55   {
    56     def length: Int = command.length
    57   }
    58 }
    59 
    60 final class Outer_Syntax private(
    61   val keywords: Keyword.Keywords = Keyword.Keywords.empty,
    62   val completion: Completion = Completion.empty,
    63   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
    64   val has_tokens: Boolean = true)
    65 {
    66   /** syntax content **/
    67 
    68   override def toString: String = keywords.toString
    69 
    70 
    71   /* add keywords */
    72 
    73   def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
    74   {
    75     val keywords1 = keywords + (name, kind, tags)
    76     val completion1 =
    77       completion.add_keyword(name).
    78         add_abbrevs(
    79           (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
    80            else Nil) :::
    81           (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
    82     new Outer_Syntax(keywords1, completion1, language_context, true)
    83   }
    84 
    85   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    86     (this /: keywords) {
    87       case (syntax, (name, ((kind, tags), _))) =>
    88         syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
    89     }
    90 
    91   def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
    92     if (abbrevs.isEmpty) this
    93     else {
    94       val completion1 =
    95         completion.add_abbrevs(
    96           (for ((a, b) <- abbrevs) yield {
    97             val a1 = Symbol.decode(a)
    98             val a2 = Symbol.encode(a)
    99             val b1 = Symbol.decode(b)
   100             List((a1, b1), (a2, b1))
   101           }).flatten)
   102       new Outer_Syntax(keywords, completion1, language_context, has_tokens)
   103     }
   104 
   105 
   106   /* merge */
   107 
   108   def ++ (other: Outer_Syntax): Outer_Syntax =
   109     if (this eq other) this
   110     else {
   111       val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
   112       val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
   113       if ((keywords eq keywords1) && (completion eq completion1)) this
   114       else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
   115     }
   116 
   117 
   118   /* load commands */
   119 
   120   def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
   121   def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
   122 
   123 
   124   /* language context */
   125 
   126   def set_language_context(context: Completion.Language_Context): Outer_Syntax =
   127     new Outer_Syntax(keywords, completion, context, has_tokens)
   128 
   129   def no_tokens: Outer_Syntax =
   130   {
   131     require(keywords.is_empty)
   132     new Outer_Syntax(
   133       completion = completion,
   134       language_context = language_context,
   135       has_tokens = false)
   136   }
   137 
   138 
   139 
   140   /** parsing **/
   141 
   142   /* command spans */
   143 
   144   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   145   {
   146     val result = new mutable.ListBuffer[Command_Span.Span]
   147     val content = new mutable.ListBuffer[Token]
   148     val improper = new mutable.ListBuffer[Token]
   149 
   150     def ship(span: List[Token])
   151     {
   152       val kind =
   153         if (span.forall(_.is_improper)) Command_Span.Ignored_Span
   154         else if (span.exists(_.is_error)) Command_Span.Malformed_Span
   155         else
   156           span.find(_.is_command) match {
   157             case None => Command_Span.Malformed_Span
   158             case Some(cmd) =>
   159               val name = cmd.source
   160               val offset =
   161                 (0 /: span.takeWhile(_ != cmd)) {
   162                   case (i, tok) => i + Symbol.iterator(tok.source).length }
   163               val end_offset = offset + Symbol.iterator(name).length
   164               val pos = Position.Range(Text.Range(offset, end_offset) + 1)
   165               Command_Span.Command_Span(name, pos)
   166           }
   167       result += Command_Span.Span(kind, span)
   168     }
   169 
   170     def flush()
   171     {
   172       if (content.nonEmpty) { ship(content.toList); content.clear }
   173       if (improper.nonEmpty) { ship(improper.toList); improper.clear }
   174     }
   175 
   176     for (tok <- toks) {
   177       if (tok.is_improper) improper += tok
   178       else if (keywords.is_before_command(tok) ||
   179         tok.is_command &&
   180           (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
   181       { flush(); content += tok }
   182       else { content ++= improper; improper.clear; content += tok }
   183     }
   184     flush()
   185 
   186     result.toList
   187   }
   188 
   189   def parse_spans(input: CharSequence): List[Command_Span.Span] =
   190     parse_spans(Token.explode(keywords, input))
   191 
   192 
   193   /* overall document structure */
   194 
   195   def heading_level(command: Command): Option[Int] =
   196   {
   197     val name = command.span.name
   198     name match {
   199       case Thy_Header.CHAPTER => Some(0)
   200       case Thy_Header.SECTION => Some(1)
   201       case Thy_Header.SUBSECTION => Some(2)
   202       case Thy_Header.SUBSUBSECTION => Some(3)
   203       case Thy_Header.PARAGRAPH => Some(4)
   204       case Thy_Header.SUBPARAGRAPH => Some(5)
   205       case _ =>
   206         keywords.kinds.get(name) match {
   207           case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
   208           case _ => None
   209         }
   210     }
   211   }
   212 
   213   def parse_document(node_name: Document.Node.Name, text: CharSequence):
   214     List[Outer_Syntax.Document] =
   215   {
   216     /* stack operations */
   217 
   218     def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
   219       new mutable.ListBuffer[Outer_Syntax.Document]
   220 
   221     var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
   222       List((0, Command.empty, buffer()))
   223 
   224     @tailrec def close(level: Int => Boolean)
   225     {
   226       stack match {
   227         case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
   228           body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
   229           stack = stack.tail
   230           close(level)
   231         case _ =>
   232       }
   233     }
   234 
   235     def result(): List[Outer_Syntax.Document] =
   236     {
   237       close(_ => true)
   238       stack.head._3.toList
   239     }
   240 
   241     def add(command: Command)
   242     {
   243       heading_level(command) match {
   244         case Some(i) =>
   245           close(_ > i)
   246           stack = (i + 1, command, buffer()) :: stack
   247         case None =>
   248       }
   249       stack.head._3 += Outer_Syntax.Document_Atom(command)
   250     }
   251 
   252 
   253     /* result structure */
   254 
   255     val spans = parse_spans(text)
   256     spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
   257     result()
   258   }
   259 }