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