src/Pure/Isar/outer_syntax.scala
author wenzelm
Thu Jan 08 20:56:39 2015 +0100 (2015-01-08)
changeset 59319 677615cba30d
parent 59122 c1dbcde94cd2
child 59684 86a76300137e
permissions -rw-r--r--
tuned;
     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): Outer_Syntax = this + (name, None, None)
    89   def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
    90   def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
    91     : Outer_Syntax =
    92   {
    93     val keywords1 =
    94       opt_kind match {
    95         case None => keywords + name
    96         case Some(kind) => keywords + (name, kind)
    97       }
    98     val completion1 =
    99       if (replace == Some("")) completion
   100       else completion + (name, replace getOrElse name)
   101     new Outer_Syntax(keywords1, completion1, language_context, true)
   102   }
   103 
   104   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
   105     (this /: keywords) {
   106       case (syntax, (name, opt_spec, replace)) =>
   107         val opt_kind = opt_spec.map(_._1)
   108         syntax +
   109           (Symbol.decode(name), opt_kind, replace) +
   110           (Symbol.encode(name), opt_kind, replace)
   111     }
   112 
   113 
   114   /* merge */
   115 
   116   def ++ (other: Prover.Syntax): Prover.Syntax =
   117     if (this eq other) this
   118     else {
   119       val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
   120       val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
   121       if ((keywords eq keywords1) && (completion eq completion1)) this
   122       else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
   123     }
   124 
   125 
   126   /* load commands */
   127 
   128   def load_command(name: String): Option[List[String]] = keywords.load_command(name)
   129   def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
   130 
   131 
   132   /* language context */
   133 
   134   def set_language_context(context: Completion.Language_Context): Outer_Syntax =
   135     new Outer_Syntax(keywords, completion, context, has_tokens)
   136 
   137   def no_tokens: Outer_Syntax =
   138   {
   139     require(keywords.is_empty)
   140     new Outer_Syntax(
   141       completion = completion,
   142       language_context = language_context,
   143       has_tokens = false)
   144   }
   145 
   146 
   147 
   148   /** parsing **/
   149 
   150   /* line-oriented structure */
   151 
   152   def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure)
   153     : Outer_Syntax.Line_Structure =
   154   {
   155     val improper1 = tokens.forall(_.is_improper)
   156     val command1 = tokens.exists(_.is_command)
   157 
   158     val depth1 =
   159       if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
   160       else if (command1) struct.after_span_depth
   161       else struct.span_depth
   162 
   163     val (span_depth1, after_span_depth1) =
   164       ((struct.span_depth, struct.after_span_depth) /: tokens) {
   165         case ((x, y), tok) =>
   166           if (tok.is_command) {
   167             if (tok.is_command_kind(keywords, Keyword.theory_goal))
   168               (2, 1)
   169             else if (tok.is_command_kind(keywords, Keyword.theory))
   170               (1, 0)
   171             else if (tok.is_command_kind(keywords, Keyword.proof_goal) || tok.is_begin_block)
   172               (y + 2, y + 1)
   173             else if (tok.is_command_kind(keywords, Keyword.qed) || tok.is_end_block)
   174               (y + 1, y - 1)
   175             else if (tok.is_command_kind(keywords, Keyword.qed_global))
   176               (1, 0)
   177             else (x, y)
   178           }
   179           else (x, y)
   180       }
   181 
   182     Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
   183   }
   184 
   185 
   186   /* command spans */
   187 
   188   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   189   {
   190     val result = new mutable.ListBuffer[Command_Span.Span]
   191     val content = new mutable.ListBuffer[Token]
   192     val improper = new mutable.ListBuffer[Token]
   193 
   194     def ship(span: List[Token])
   195     {
   196       val kind =
   197         if (span.nonEmpty && span.head.is_command && !span.exists(_.is_error)) {
   198           val name = span.head.source
   199           val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
   200           Command_Span.Command_Span(name, pos)
   201         }
   202         else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
   203         else Command_Span.Malformed_Span
   204       result += Command_Span.Span(kind, span)
   205     }
   206 
   207     def flush()
   208     {
   209       if (content.nonEmpty) { ship(content.toList); content.clear }
   210       if (improper.nonEmpty) { ship(improper.toList); improper.clear }
   211     }
   212 
   213     for (tok <- toks) {
   214       if (tok.is_command) { flush(); content += tok }
   215       else if (tok.is_improper) improper += tok
   216       else { content ++= improper; improper.clear; content += tok }
   217     }
   218     flush()
   219 
   220     result.toList
   221   }
   222 
   223   def parse_spans(input: CharSequence): List[Command_Span.Span] =
   224     parse_spans(Token.explode(keywords, input))
   225 
   226 
   227   /* overall document structure */
   228 
   229   def heading_level(command: Command): Option[Int] =
   230   {
   231     command.name match {
   232       case "chapter" => Some(0)
   233       case "section" | "header" => Some(1)
   234       case "subsection" => Some(2)
   235       case "subsubsection" => Some(3)
   236       case _ =>
   237         keywords.command_kind(command.name) match {
   238           case Some(kind) if Keyword.theory(kind) && kind != Keyword.THY_END => Some(4)
   239           case _ => None
   240         }
   241     }
   242   }
   243 
   244   def parse_document(node_name: Document.Node.Name, text: CharSequence):
   245     List[Outer_Syntax.Document] =
   246   {
   247     /* stack operations */
   248 
   249     def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
   250       new mutable.ListBuffer[Outer_Syntax.Document]
   251 
   252     var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
   253       List((0, Command.empty, buffer()))
   254 
   255     @tailrec def close(level: Int => Boolean)
   256     {
   257       stack match {
   258         case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
   259           body2 += Outer_Syntax.Document_Block(command.name, command.source, body.toList)
   260           stack = stack.tail
   261           close(level)
   262         case _ =>
   263       }
   264     }
   265 
   266     def result(): List[Outer_Syntax.Document] =
   267     {
   268       close(_ => true)
   269       stack.head._3.toList
   270     }
   271 
   272     def add(command: Command)
   273     {
   274       heading_level(command) match {
   275         case Some(i) =>
   276           close(_ > i)
   277           stack = (i + 1, command, buffer()) :: stack
   278         case None =>
   279       }
   280       stack.head._3 += Outer_Syntax.Document_Atom(command)
   281     }
   282 
   283 
   284     /* result structure */
   285 
   286     val spans = parse_spans(text)
   287     spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
   288     result()
   289   }
   290 }