src/Pure/Isar/document_structure.scala
changeset 63610 4b40b8196dc7
parent 63607 7246254d558f
child 63666 ff6caffcaed4
     1.1 --- a/src/Pure/Isar/document_structure.scala	Thu Aug 04 21:30:20 2016 +0200
     1.2 +++ b/src/Pure/Isar/document_structure.scala	Fri Aug 05 16:30:53 2016 +0200
     1.3 @@ -13,14 +13,12 @@
     1.4  
     1.5  object Document_Structure
     1.6  {
     1.7 -  /* general structure */
     1.8 +  /** general structure **/
     1.9  
    1.10    sealed abstract class Document { def length: Int }
    1.11    case class Block(name: String, text: String, body: List[Document]) extends Document
    1.12    { val length: Int = (0 /: body)(_ + _.length) }
    1.13 -  case class Atom(command: Command) extends Document
    1.14 -  { def length: Int = command.length }
    1.15 -
    1.16 +  case class Atom(length: Int) extends Document
    1.17  
    1.18    private def is_theory_command(keywords: Keyword.Keywords, name: String): Boolean =
    1.19      keywords.kinds.get(name) match {
    1.20 @@ -28,23 +26,9 @@
    1.21        case None => false
    1.22      }
    1.23  
    1.24 -  private def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
    1.25 -  {
    1.26 -    val name = command.span.name
    1.27 -    name match {
    1.28 -      case Thy_Header.CHAPTER => Some(0)
    1.29 -      case Thy_Header.SECTION => Some(1)
    1.30 -      case Thy_Header.SUBSECTION => Some(2)
    1.31 -      case Thy_Header.SUBSUBSECTION => Some(3)
    1.32 -      case Thy_Header.PARAGRAPH => Some(4)
    1.33 -      case Thy_Header.SUBPARAGRAPH => Some(5)
    1.34 -      case _ if is_theory_command(keywords, name) => Some(6)
    1.35 -      case _ => None
    1.36 -    }
    1.37 -  }
    1.38  
    1.39  
    1.40 -  /* context blocks */
    1.41 +  /** context blocks **/
    1.42  
    1.43    def parse_blocks(
    1.44      syntax: Outer_Syntax,
    1.45 @@ -88,7 +72,7 @@
    1.46        if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
    1.47        else if (command.span.is_end) { flush(); close() }
    1.48  
    1.49 -      stack.head._2 += Atom(command)
    1.50 +      stack.head._2 += Atom(command.source.length)
    1.51      }
    1.52  
    1.53  
    1.54 @@ -100,25 +84,30 @@
    1.55    }
    1.56  
    1.57  
    1.58 -  /* section headings etc. */
    1.59  
    1.60 -  def parse_sections(
    1.61 -    syntax: Outer_Syntax,
    1.62 -    node_name: Document.Node.Name,
    1.63 -    text: CharSequence): List[Document] =
    1.64 +  /** section headings **/
    1.65 +
    1.66 +  trait Item
    1.67    {
    1.68 -    /* stack operations */
    1.69 +    def name: String = ""
    1.70 +    def source: String = ""
    1.71 +    def heading_level: Option[Int] = None
    1.72 +  }
    1.73  
    1.74 -    def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
    1.75 +  object No_Item extends Item
    1.76  
    1.77 -    var stack: List[(Int, Command, mutable.ListBuffer[Document])] =
    1.78 -      List((0, Command.empty, buffer()))
    1.79 +  class Sections(keywords: Keyword.Keywords)
    1.80 +  {
    1.81 +    private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
    1.82  
    1.83 -    @tailrec def close(level: Int => Boolean)
    1.84 +    private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
    1.85 +      List((0, No_Item, buffer()))
    1.86 +
    1.87 +    @tailrec private def close(level: Int => Boolean)
    1.88      {
    1.89        stack match {
    1.90 -        case (lev, command, body) :: (_, _, body2) :: _ if level(lev) =>
    1.91 -          body2 += Block(command.span.name, command.source, body.toList)
    1.92 +        case (lev, item, body) :: (_, _, body2) :: _ if level(lev) =>
    1.93 +          body2 += Block(item.name, item.source, body.toList)
    1.94            stack = stack.tail
    1.95            close(level)
    1.96          case _ =>
    1.97 @@ -131,22 +120,91 @@
    1.98        stack.head._3.toList
    1.99      }
   1.100  
   1.101 -    def add(command: Command)
   1.102 +    def add(item: Item)
   1.103      {
   1.104 -      heading_level(syntax.keywords, command) match {
   1.105 +      item.heading_level match {
   1.106          case Some(i) =>
   1.107            close(_ > i)
   1.108 -          stack = (i + 1, command, buffer()) :: stack
   1.109 +          stack = (i + 1, item, buffer()) :: stack
   1.110          case None =>
   1.111        }
   1.112 -      stack.head._3 += Atom(command)
   1.113 +      stack.head._3 += Atom(item.source.length)
   1.114      }
   1.115 +  }
   1.116  
   1.117  
   1.118 -    /* result structure */
   1.119 +  /* outer syntax sections */
   1.120 +
   1.121 +  private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item
   1.122 +  {
   1.123 +    override def name: String = command.span.name
   1.124 +    override def source: String = command.source
   1.125 +    override def heading_level: Option[Int] =
   1.126 +    {
   1.127 +      name match {
   1.128 +        case Thy_Header.CHAPTER => Some(0)
   1.129 +        case Thy_Header.SECTION => Some(1)
   1.130 +        case Thy_Header.SUBSECTION => Some(2)
   1.131 +        case Thy_Header.SUBSUBSECTION => Some(3)
   1.132 +        case Thy_Header.PARAGRAPH => Some(4)
   1.133 +        case Thy_Header.SUBPARAGRAPH => Some(5)
   1.134 +        case _ if is_theory_command(keywords, name) => Some(6)
   1.135 +        case _ => None
   1.136 +      }
   1.137 +    }
   1.138 +  }
   1.139 +
   1.140 +  def parse_sections(
   1.141 +    syntax: Outer_Syntax,
   1.142 +    node_name: Document.Node.Name,
   1.143 +    text: CharSequence): List[Document] =
   1.144 +  {
   1.145 +    val sections = new Sections(syntax.keywords)
   1.146 +
   1.147 +    for { span <- syntax.parse_spans(text) } {
   1.148 +      sections.add(
   1.149 +        new Command_Item(syntax.keywords,
   1.150 +          Command(Document_ID.none, node_name, Command.no_blobs, span)))
   1.151 +    }
   1.152 +    sections.result()
   1.153 +  }
   1.154 +
   1.155  
   1.156 -    val spans = syntax.parse_spans(text)
   1.157 -    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
   1.158 -    result()
   1.159 +  /* ML sections */
   1.160 +
   1.161 +  private class ML_Item(token: ML_Lex.Token, level: Option[Int]) extends Item
   1.162 +  {
   1.163 +    override def source: String = token.source
   1.164 +    override def heading_level: Option[Int] = level
   1.165 +  }
   1.166 +
   1.167 +  def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] =
   1.168 +  {
   1.169 +    val sections = new Sections(Keyword.Keywords.empty)
   1.170 +    val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None)
   1.171 +
   1.172 +    var context: Scan.Line_Context = Scan.Finished
   1.173 +    for (line <- Library.separated_chunks(_ == '\n', text)) {
   1.174 +      val (toks, next_context) = ML_Lex.tokenize_line(SML, line, context)
   1.175 +      val level =
   1.176 +        toks.filterNot(_.is_space) match {
   1.177 +          case List(tok) if tok.is_comment =>
   1.178 +            val s = tok.source
   1.179 +            if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
   1.180 +            else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
   1.181 +            else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
   1.182 +            else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
   1.183 +            else None
   1.184 +          case _ => None
   1.185 +        }
   1.186 +      if (level.isDefined && context == Scan.Finished && next_context == Scan.Finished)
   1.187 +        toks.foreach(tok => sections.add(new ML_Item(tok, if (tok.is_comment) level else None)))
   1.188 +      else
   1.189 +        toks.foreach(tok => sections.add(new ML_Item(tok, None)))
   1.190 +
   1.191 +      sections.add(nl)
   1.192 +      context = next_context
   1.193 +    }
   1.194 +    sections.result()
   1.195    }
   1.196  }