wenzelm@34166: /*  Title:      Pure/Isar/outer_syntax.scala
wenzelm@34166:     Author:     Makarius
wenzelm@34166: 
wenzelm@34166: Isabelle/Isar outer syntax.
wenzelm@34166: */
wenzelm@34166: 
wenzelm@34166: package isabelle
wenzelm@34166: 
wenzelm@34166: 
wenzelm@43411: import scala.collection.mutable
wenzelm@34166: 
wenzelm@34166: 
wenzelm@43774: object Outer_Syntax
wenzelm@43774: {
wenzelm@58706:   /* syntax */
wenzelm@58706: 
wenzelm@58706:   val empty: Outer_Syntax = new Outer_Syntax()
wenzelm@58706: 
wenzelm@58706:   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
wenzelm@58706: 
wenzelm@66776:   def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
wenzelm@66717: 
wenzelm@58706: 
wenzelm@58706:   /* string literals */
wenzelm@58706: 
wenzelm@43774:   def quote_string(str: String): String =
wenzelm@43774:   {
wenzelm@43774:     val result = new StringBuilder(str.length + 10)
wenzelm@43774:     result += '"'
wenzelm@43774:     for (s <- Symbol.iterator(str)) {
wenzelm@43774:       if (s.length == 1) {
wenzelm@43774:         val c = s(0)
wenzelm@43774:         if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
wenzelm@43774:           result += '\\'
wenzelm@43774:           if (c < 10) result += '0'
wenzelm@43774:           if (c < 100) result += '0'
wenzelm@60215:           result ++= c.asInstanceOf[Int].toString
wenzelm@43774:         }
wenzelm@43774:         else result += c
wenzelm@43774:       }
wenzelm@43774:       else result ++= s
wenzelm@43774:     }
wenzelm@43774:     result += '"'
wenzelm@43774:     result.toString
wenzelm@43774:   }
wenzelm@43774: }
wenzelm@43774: 
wenzelm@46712: final class Outer_Syntax private(
wenzelm@58900:   val keywords: Keyword.Keywords = Keyword.Keywords.empty,
wenzelm@53280:   val completion: Completion = Completion.empty,
wenzelm@63867:   val rev_abbrevs: Thy_Header.Abbrevs = Nil,
wenzelm@55749:   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
wenzelm@63584:   val has_tokens: Boolean = true)
wenzelm@34166: {
wenzelm@58706:   /** syntax content **/
wenzelm@58706: 
wenzelm@58900:   override def toString: String = keywords.toString
wenzelm@56393: 
wenzelm@58695: 
wenzelm@63867:   /* keywords */
wenzelm@58695: 
wenzelm@65383:   def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
wenzelm@53280:   {
wenzelm@65383:     val keywords1 = keywords + (name, kind, exts)
wenzelm@53280:     val completion1 =
wenzelm@63587:       completion.add_keyword(name).
wenzelm@63587:         add_abbrevs(
wenzelm@63587:           (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
wenzelm@63587:            else Nil) :::
wenzelm@63587:           (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
wenzelm@63867:     new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
wenzelm@53280:   }
wenzelm@48706: 
wenzelm@48873:   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
wenzelm@48873:     (this /: keywords) {
wenzelm@65384:       case (syntax, (name, spec)) =>
wenzelm@65384:         syntax +
wenzelm@65384:           (Symbol.decode(name), spec.kind, spec.exts) +
wenzelm@65384:           (Symbol.encode(name), spec.kind, spec.exts)
wenzelm@63579:     }
wenzelm@63579: 
wenzelm@63867: 
wenzelm@63867:   /* abbrevs */
wenzelm@63867: 
wenzelm@63867:   def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse
wenzelm@63867: 
wenzelm@63867:   def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
wenzelm@63867:     if (new_abbrevs.isEmpty) this
wenzelm@63579:     else {
wenzelm@63579:       val completion1 =
wenzelm@63579:         completion.add_abbrevs(
wenzelm@63867:           (for ((a, b) <- new_abbrevs) yield {
wenzelm@63579:             val a1 = Symbol.decode(a)
wenzelm@63579:             val a2 = Symbol.encode(a)
wenzelm@63579:             val b1 = Symbol.decode(b)
wenzelm@63579:             List((a1, b1), (a2, b1))
wenzelm@63579:           }).flatten)
wenzelm@63867:       val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
wenzelm@63867:       new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens)
wenzelm@46940:     }
wenzelm@34166: 
wenzelm@58695: 
wenzelm@66717:   /* build */
wenzelm@66717: 
wenzelm@66717:   def + (header: Document.Node.Header): Outer_Syntax =
wenzelm@66717:     add_keywords(header.keywords).add_abbrevs(header.abbrevs)
wenzelm@59073: 
wenzelm@63584:   def ++ (other: Outer_Syntax): Outer_Syntax =
wenzelm@59073:     if (this eq other) this
wenzelm@66776:     else if (this eq Outer_Syntax.empty) other
wenzelm@59073:     else {
wenzelm@63865:       val keywords1 = keywords ++ other.keywords
wenzelm@63865:       val completion1 = completion ++ other.completion
wenzelm@63867:       val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
wenzelm@59077:       if ((keywords eq keywords1) && (completion eq completion1)) this
wenzelm@63867:       else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
wenzelm@59073:     }
wenzelm@59073: 
wenzelm@59073: 
wenzelm@59735:   /* load commands */
wenzelm@58900: 
wenzelm@63441:   def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
wenzelm@58900:   def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
wenzelm@58900: 
wenzelm@58900: 
wenzelm@58706:   /* language context */
wenzelm@34166: 
wenzelm@58706:   def set_language_context(context: Completion.Language_Context): Outer_Syntax =
wenzelm@63867:     new Outer_Syntax(keywords, completion, rev_abbrevs, context, has_tokens)
wenzelm@58706: 
wenzelm@58706:   def no_tokens: Outer_Syntax =
wenzelm@46969:   {
wenzelm@58900:     require(keywords.is_empty)
wenzelm@58706:     new Outer_Syntax(
wenzelm@58706:       completion = completion,
wenzelm@63867:       rev_abbrevs = rev_abbrevs,
wenzelm@58706:       language_context = language_context,
wenzelm@58706:       has_tokens = false)
wenzelm@46969:   }
wenzelm@40454: 
wenzelm@58706: 
wenzelm@40454: 
wenzelm@58706:   /** parsing **/
wenzelm@34166: 
wenzelm@58706:   /* command spans */
wenzelm@57905: 
wenzelm@57905:   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
wenzelm@57905:   {
wenzelm@57905:     val result = new mutable.ListBuffer[Command_Span.Span]
wenzelm@57905:     val content = new mutable.ListBuffer[Token]
wenzelm@57905:     val improper = new mutable.ListBuffer[Token]
wenzelm@57905: 
wenzelm@57905:     def ship(span: List[Token])
wenzelm@57905:     {
wenzelm@57905:       val kind =
wenzelm@59924:         if (span.forall(_.is_improper)) Command_Span.Ignored_Span
wenzelm@59924:         else if (span.exists(_.is_error)) Command_Span.Malformed_Span
wenzelm@59924:         else
wenzelm@59924:           span.find(_.is_command) match {
wenzelm@59924:             case None => Command_Span.Malformed_Span
wenzelm@59924:             case Some(cmd) =>
wenzelm@59924:               val name = cmd.source
wenzelm@59924:               val offset =
wenzelm@59924:                 (0 /: span.takeWhile(_ != cmd)) {
wenzelm@64616:                   case (i, tok) => i + Symbol.length(tok.source) }
wenzelm@64616:               val end_offset = offset + Symbol.length(name)
wenzelm@59924:               val pos = Position.Range(Text.Range(offset, end_offset) + 1)
wenzelm@59924:               Command_Span.Command_Span(name, pos)
wenzelm@59924:           }
wenzelm@57905:       result += Command_Span.Span(kind, span)
wenzelm@57905:     }
wenzelm@57905: 
wenzelm@57905:     def flush()
wenzelm@57905:     {
wenzelm@59319:       if (content.nonEmpty) { ship(content.toList); content.clear }
wenzelm@59319:       if (improper.nonEmpty) { ship(improper.toList); improper.clear }
wenzelm@57905:     }
wenzelm@57905: 
wenzelm@57905:     for (tok <- toks) {
wenzelm@59924:       if (tok.is_improper) improper += tok
wenzelm@63441:       else if (keywords.is_before_command(tok) ||
wenzelm@63441:         tok.is_command &&
wenzelm@63441:           (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
wenzelm@59924:       { flush(); content += tok }
wenzelm@57905:       else { content ++= improper; improper.clear; content += tok }
wenzelm@57905:     }
wenzelm@57905:     flush()
wenzelm@57905: 
wenzelm@57905:     result.toList
wenzelm@57905:   }
wenzelm@57905: 
wenzelm@57906:   def parse_spans(input: CharSequence): List[Command_Span.Span] =
wenzelm@59083:     parse_spans(Token.explode(keywords, input))
wenzelm@34166: }