src/Pure/Isar/outer_syntax.scala
author wenzelm
Wed Aug 03 11:45:09 2016 +0200 (2016-08-03)
changeset 63592 64db21931bcb
parent 63587 881e8e2cfec2
child 63603 9d9ea2c6bc38
permissions -rw-r--r--
include 'begin' and 'end' structure in text folds;
     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   /* line-oriented structure */
    48 
    49   object Line_Structure
    50   {
    51     val init = Line_Structure()
    52   }
    53 
    54   sealed case class Line_Structure(
    55     improper: Boolean = true,
    56     command: Boolean = false,
    57     depth: Int = 0,
    58     span_depth: Int = 0,
    59     after_span_depth: Int = 0,
    60     element_depth: Int = 0)
    61 
    62 
    63   /* overall document structure */
    64 
    65   sealed abstract class Document { def length: Int }
    66   case class Document_Block(name: String, text: String, body: List[Document]) extends Document
    67   {
    68     val length: Int = (0 /: body)(_ + _.length)
    69   }
    70   case class Document_Atom(command: Command) extends Document
    71   {
    72     def length: Int = command.length
    73   }
    74 }
    75 
    76 final class Outer_Syntax private(
    77   val keywords: Keyword.Keywords = Keyword.Keywords.empty,
    78   val completion: Completion = Completion.empty,
    79   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
    80   val has_tokens: Boolean = true)
    81 {
    82   /** syntax content **/
    83 
    84   override def toString: String = keywords.toString
    85 
    86 
    87   /* add keywords */
    88 
    89   def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
    90   {
    91     val keywords1 = keywords + (name, kind, tags)
    92     val completion1 =
    93       completion.add_keyword(name).
    94         add_abbrevs(
    95           (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
    96            else Nil) :::
    97           (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
    98     new Outer_Syntax(keywords1, completion1, language_context, true)
    99   }
   100 
   101   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
   102     (this /: keywords) {
   103       case (syntax, (name, ((kind, tags), _))) =>
   104         syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
   105     }
   106 
   107   def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
   108     if (abbrevs.isEmpty) this
   109     else {
   110       val completion1 =
   111         completion.add_abbrevs(
   112           (for ((a, b) <- abbrevs) yield {
   113             val a1 = Symbol.decode(a)
   114             val a2 = Symbol.encode(a)
   115             val b1 = Symbol.decode(b)
   116             List((a1, b1), (a2, b1))
   117           }).flatten)
   118       new Outer_Syntax(keywords, completion1, language_context, has_tokens)
   119     }
   120 
   121 
   122   /* merge */
   123 
   124   def ++ (other: Outer_Syntax): Outer_Syntax =
   125     if (this eq other) this
   126     else {
   127       val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
   128       val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
   129       if ((keywords eq keywords1) && (completion eq completion1)) this
   130       else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
   131     }
   132 
   133 
   134   /* load commands */
   135 
   136   def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
   137   def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
   138 
   139 
   140   /* language context */
   141 
   142   def set_language_context(context: Completion.Language_Context): Outer_Syntax =
   143     new Outer_Syntax(keywords, completion, context, has_tokens)
   144 
   145   def no_tokens: Outer_Syntax =
   146   {
   147     require(keywords.is_empty)
   148     new Outer_Syntax(
   149       completion = completion,
   150       language_context = language_context,
   151       has_tokens = false)
   152   }
   153 
   154 
   155 
   156   /** parsing **/
   157 
   158   /* line-oriented structure */
   159 
   160   private val close_structure =
   161     Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE, Keyword.THY_END)
   162 
   163   def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
   164     : Outer_Syntax.Line_Structure =
   165   {
   166     val improper1 = tokens.forall(_.is_improper)
   167     val command1 = tokens.exists(_.is_begin_or_command)
   168 
   169     val command_depth =
   170       tokens.iterator.filter(_.is_proper).toStream.headOption match {
   171         case Some(tok) =>
   172           if (keywords.is_command(tok, close_structure))
   173             Some(structure.after_span_depth - 1)
   174           else None
   175         case None => None
   176       }
   177 
   178     val depth0 = structure.element_depth
   179     val depth1 =
   180       if (tokens.exists(tok =>
   181             keywords.is_before_command(tok) ||
   182             !tok.is_end && keywords.is_command(tok, Keyword.theory))) depth0
   183       else if (command_depth.isDefined) command_depth.get
   184       else if (command1) structure.after_span_depth
   185       else structure.span_depth
   186 
   187     val (span_depth1, after_span_depth1, element_depth1) =
   188       ((structure.span_depth, structure.after_span_depth, structure.element_depth) /: tokens) {
   189         case (depths @ (x, y, z), tok) =>
   190           if (tok.is_begin) (z + 2, z + 1, z + 1)
   191           else if (tok.is_end) (z + 1, z - 1, z - 1)
   192           else if (tok.is_command) {
   193             if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
   194             else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
   195             else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
   196             else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
   197             else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
   198             else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
   199             else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
   200             else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
   201             else depths
   202           }
   203           else depths
   204       }
   205 
   206     Outer_Syntax.Line_Structure(
   207       improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
   208   }
   209 
   210 
   211   /* command spans */
   212 
   213   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   214   {
   215     val result = new mutable.ListBuffer[Command_Span.Span]
   216     val content = new mutable.ListBuffer[Token]
   217     val improper = new mutable.ListBuffer[Token]
   218 
   219     def ship(span: List[Token])
   220     {
   221       val kind =
   222         if (span.forall(_.is_improper)) Command_Span.Ignored_Span
   223         else if (span.exists(_.is_error)) Command_Span.Malformed_Span
   224         else
   225           span.find(_.is_command) match {
   226             case None => Command_Span.Malformed_Span
   227             case Some(cmd) =>
   228               val name = cmd.source
   229               val offset =
   230                 (0 /: span.takeWhile(_ != cmd)) {
   231                   case (i, tok) => i + Symbol.iterator(tok.source).length }
   232               val end_offset = offset + Symbol.iterator(name).length
   233               val pos = Position.Range(Text.Range(offset, end_offset) + 1)
   234               Command_Span.Command_Span(name, pos)
   235           }
   236       result += Command_Span.Span(kind, span)
   237     }
   238 
   239     def flush()
   240     {
   241       if (content.nonEmpty) { ship(content.toList); content.clear }
   242       if (improper.nonEmpty) { ship(improper.toList); improper.clear }
   243     }
   244 
   245     for (tok <- toks) {
   246       if (tok.is_improper) improper += tok
   247       else if (keywords.is_before_command(tok) ||
   248         tok.is_command &&
   249           (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
   250       { flush(); content += tok }
   251       else { content ++= improper; improper.clear; content += tok }
   252     }
   253     flush()
   254 
   255     result.toList
   256   }
   257 
   258   def parse_spans(input: CharSequence): List[Command_Span.Span] =
   259     parse_spans(Token.explode(keywords, input))
   260 
   261 
   262   /* overall document structure */
   263 
   264   def heading_level(command: Command): Option[Int] =
   265   {
   266     val name = command.span.name
   267     name match {
   268       case Thy_Header.CHAPTER => Some(0)
   269       case Thy_Header.SECTION => Some(1)
   270       case Thy_Header.SUBSECTION => Some(2)
   271       case Thy_Header.SUBSUBSECTION => Some(3)
   272       case Thy_Header.PARAGRAPH => Some(4)
   273       case Thy_Header.SUBPARAGRAPH => Some(5)
   274       case _ =>
   275         keywords.kinds.get(name) match {
   276           case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
   277           case _ => None
   278         }
   279     }
   280   }
   281 
   282   def parse_document(node_name: Document.Node.Name, text: CharSequence):
   283     List[Outer_Syntax.Document] =
   284   {
   285     /* stack operations */
   286 
   287     def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
   288       new mutable.ListBuffer[Outer_Syntax.Document]
   289 
   290     var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
   291       List((0, Command.empty, buffer()))
   292 
   293     @tailrec def close(level: Int => Boolean)
   294     {
   295       stack match {
   296         case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
   297           body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
   298           stack = stack.tail
   299           close(level)
   300         case _ =>
   301       }
   302     }
   303 
   304     def result(): List[Outer_Syntax.Document] =
   305     {
   306       close(_ => true)
   307       stack.head._3.toList
   308     }
   309 
   310     def add(command: Command)
   311     {
   312       heading_level(command) match {
   313         case Some(i) =>
   314           close(_ > i)
   315           stack = (i + 1, command, buffer()) :: stack
   316         case None =>
   317       }
   318       stack.head._3 += Outer_Syntax.Document_Atom(command)
   319     }
   320 
   321 
   322     /* result structure */
   323 
   324     val spans = parse_spans(text)
   325     spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
   326     result()
   327   }
   328 }