src/Pure/Isar/outer_syntax.scala
changeset 58706 70a947611792
parent 58703 883efcc7a50d
child 58743 c07a59140fee
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 22:50:35 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Oct 19 11:20:03 2014 +0200
     1.3 @@ -9,10 +9,20 @@
     1.4  
     1.5  import scala.util.parsing.input.{Reader, CharSequenceReader}
     1.6  import scala.collection.mutable
     1.7 +import scala.annotation.tailrec
     1.8  
     1.9  
    1.10  object Outer_Syntax
    1.11  {
    1.12 +  /* syntax */
    1.13 +
    1.14 +  val empty: Outer_Syntax = new Outer_Syntax()
    1.15 +
    1.16 +  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
    1.17 +
    1.18 +
    1.19 +  /* string literals */
    1.20 +
    1.21    def quote_string(str: String): String =
    1.22    {
    1.23      val result = new StringBuilder(str.length + 10)
    1.24 @@ -34,10 +44,6 @@
    1.25      result.toString
    1.26    }
    1.27  
    1.28 -  val empty: Outer_Syntax = new Outer_Syntax()
    1.29 -
    1.30 -  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
    1.31 -
    1.32  
    1.33    /* line-oriented structure */
    1.34  
    1.35 @@ -52,6 +58,19 @@
    1.36      depth: Int = 0,
    1.37      span_depth: Int = 0,
    1.38      after_span_depth: Int = 0)
    1.39 +
    1.40 +
    1.41 +  /* overall document structure */
    1.42 +
    1.43 +  sealed abstract class Document { def length: Int }
    1.44 +  case class Document_Block(val name: String, val body: List[Document]) extends Document
    1.45 +  {
    1.46 +    val length: Int = (0 /: body)(_ + _.length)
    1.47 +  }
    1.48 +  case class Document_Atom(val command: Command) extends Document
    1.49 +  {
    1.50 +    def length: Int = command.length
    1.51 +  }
    1.52  }
    1.53  
    1.54  final class Outer_Syntax private(
    1.55 @@ -61,6 +80,8 @@
    1.56    val language_context: Completion.Language_Context = Completion.Language_Context.outer,
    1.57    val has_tokens: Boolean = true) extends Prover.Syntax
    1.58  {
    1.59 +  /** syntax content **/
    1.60 +
    1.61    override def toString: String =
    1.62      (for ((name, (kind, files)) <- keywords) yield {
    1.63        if (kind == Keyword.MINOR) quote(name)
    1.64 @@ -134,24 +155,23 @@
    1.65      }
    1.66  
    1.67  
    1.68 -  /* document headings */
    1.69 +  /* language context */
    1.70  
    1.71 -  def heading_level(name: String): Option[Int] =
    1.72 +  def set_language_context(context: Completion.Language_Context): Outer_Syntax =
    1.73 +    new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
    1.74 +
    1.75 +  def no_tokens: Outer_Syntax =
    1.76    {
    1.77 -    keyword_kind(name) match {
    1.78 -      case _ if name == "header" => Some(0)
    1.79 -      case Some(Keyword.THY_HEADING1) => Some(1)
    1.80 -      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
    1.81 -      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
    1.82 -      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
    1.83 -      case Some(kind) if Keyword.theory(kind) => Some(5)
    1.84 -      case _ => None
    1.85 -    }
    1.86 +    require(keywords.isEmpty && lexicon.isEmpty)
    1.87 +    new Outer_Syntax(
    1.88 +      completion = completion,
    1.89 +      language_context = language_context,
    1.90 +      has_tokens = false)
    1.91    }
    1.92  
    1.93 -  def heading_level(command: Command): Option[Int] =
    1.94 -    heading_level(command.name)
    1.95 +
    1.96  
    1.97 +  /** parsing **/
    1.98  
    1.99    /* line-oriented structure */
   1.100  
   1.101 @@ -217,7 +237,7 @@
   1.102    }
   1.103  
   1.104  
   1.105 -  /* parse_spans */
   1.106 +  /* command spans */
   1.107  
   1.108    def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   1.109    {
   1.110 @@ -258,17 +278,65 @@
   1.111      parse_spans(scan(input))
   1.112  
   1.113  
   1.114 -  /* language context */
   1.115 +  /* overall document structure */
   1.116  
   1.117 -  def set_language_context(context: Completion.Language_Context): Outer_Syntax =
   1.118 -    new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
   1.119 +  def heading_level(command: Command): Option[Int] =
   1.120 +  {
   1.121 +    keyword_kind(command.name) match {
   1.122 +      case _ if command.name == "header" => Some(0)
   1.123 +      case Some(Keyword.THY_HEADING1) => Some(1)
   1.124 +      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
   1.125 +      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
   1.126 +      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
   1.127 +      case Some(kind) if Keyword.theory(kind) => Some(5)
   1.128 +      case _ => None
   1.129 +    }
   1.130 +  }
   1.131 +
   1.132 +  def parse_document(node_name: Document.Node.Name, text: CharSequence): Outer_Syntax.Document =
   1.133 +  {
   1.134 +    /* stack operations */
   1.135 +
   1.136 +    def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
   1.137 +      new mutable.ListBuffer[Outer_Syntax.Document]
   1.138 +
   1.139 +    var stack: List[(Int, String, mutable.ListBuffer[Outer_Syntax.Document])] =
   1.140 +      List((0, node_name.toString, buffer()))
   1.141  
   1.142 -  def no_tokens: Outer_Syntax =
   1.143 -  {
   1.144 -    require(keywords.isEmpty && lexicon.isEmpty)
   1.145 -    new Outer_Syntax(
   1.146 -      completion = completion,
   1.147 -      language_context = language_context,
   1.148 -      has_tokens = false)
   1.149 +    @tailrec def close(level: Int => Boolean)
   1.150 +    {
   1.151 +      stack match {
   1.152 +        case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
   1.153 +          body2 += Outer_Syntax.Document_Block(name, body.toList)
   1.154 +          stack = stack.tail
   1.155 +          close(level)
   1.156 +        case _ =>
   1.157 +      }
   1.158 +    }
   1.159 +
   1.160 +    def result(): Outer_Syntax.Document =
   1.161 +    {
   1.162 +      close(_ => true)
   1.163 +      val (_, name, body) = stack.head
   1.164 +      Outer_Syntax.Document_Block(name, body.toList)
   1.165 +    }
   1.166 +
   1.167 +    def add(command: Command)
   1.168 +    {
   1.169 +      heading_level(command) match {
   1.170 +        case Some(i) =>
   1.171 +          close(_ > i)
   1.172 +          stack = (i + 1, command.source, buffer()) :: stack
   1.173 +        case None =>
   1.174 +      }
   1.175 +      stack.head._3 += Outer_Syntax.Document_Atom(command)
   1.176 +    }
   1.177 +
   1.178 +
   1.179 +    /* result structure */
   1.180 +
   1.181 +    val spans = parse_spans(text)
   1.182 +    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
   1.183 +    result()
   1.184    }
   1.185  }