src/Pure/Isar/document_structure.scala
author wenzelm
Fri Aug 05 16:30:53 2016 +0200 (2016-08-05)
changeset 63610 4b40b8196dc7
parent 63607 7246254d558f
child 63666 ff6caffcaed4
permissions -rw-r--r--
Sidekick parser for isabelle-ml and sml mode;
     1 /*  Title:      Pure/Isar/document_structure.scala
     2     Author:     Makarius
     3 
     4 Overall document structure.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.mutable
    11 import scala.annotation.tailrec
    12 
    13 
    14 object Document_Structure
    15 {
    16   /** general structure **/
    17 
    18   sealed abstract class Document { def length: Int }
    19   case class Block(name: String, text: String, body: List[Document]) extends Document
    20   { val length: Int = (0 /: body)(_ + _.length) }
    21   case class Atom(length: Int) extends Document
    22 
    23   private def is_theory_command(keywords: Keyword.Keywords, name: String): Boolean =
    24     keywords.kinds.get(name) match {
    25       case Some(kind) => Keyword.theory(kind) && !Keyword.theory_end(kind)
    26       case None => false
    27     }
    28 
    29 
    30 
    31   /** context blocks **/
    32 
    33   def parse_blocks(
    34     syntax: Outer_Syntax,
    35     node_name: Document.Node.Name,
    36     text: CharSequence): List[Document] =
    37   {
    38     def is_plain_theory(command: Command): Boolean =
    39       is_theory_command(syntax.keywords, command.span.name) &&
    40       !command.span.is_begin && !command.span.is_end
    41 
    42 
    43     /* stack operations */
    44 
    45     def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
    46 
    47     var stack: List[(Command, mutable.ListBuffer[Document])] =
    48       List((Command.empty, buffer()))
    49 
    50     def open(command: Command) { stack = (command, buffer()) :: stack }
    51 
    52     def close(): Boolean =
    53       stack match {
    54         case (command, body) :: (_, body2) :: _ =>
    55           body2 += Block(command.span.name, command.source, body.toList)
    56           stack = stack.tail
    57           true
    58         case _ =>
    59           false
    60       }
    61 
    62     def flush() { if (is_plain_theory(stack.head._1)) close() }
    63 
    64     def result(): List[Document] =
    65     {
    66       while (close()) { }
    67       stack.head._2.toList
    68     }
    69 
    70     def add(command: Command)
    71     {
    72       if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
    73       else if (command.span.is_end) { flush(); close() }
    74 
    75       stack.head._2 += Atom(command.source.length)
    76     }
    77 
    78 
    79     /* result structure */
    80 
    81     val spans = syntax.parse_spans(text)
    82     spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
    83     result()
    84   }
    85 
    86 
    87 
    88   /** section headings **/
    89 
    90   trait Item
    91   {
    92     def name: String = ""
    93     def source: String = ""
    94     def heading_level: Option[Int] = None
    95   }
    96 
    97   object No_Item extends Item
    98 
    99   class Sections(keywords: Keyword.Keywords)
   100   {
   101     private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
   102 
   103     private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
   104       List((0, No_Item, buffer()))
   105 
   106     @tailrec private def close(level: Int => Boolean)
   107     {
   108       stack match {
   109         case (lev, item, body) :: (_, _, body2) :: _ if level(lev) =>
   110           body2 += Block(item.name, item.source, body.toList)
   111           stack = stack.tail
   112           close(level)
   113         case _ =>
   114       }
   115     }
   116 
   117     def result(): List[Document] =
   118     {
   119       close(_ => true)
   120       stack.head._3.toList
   121     }
   122 
   123     def add(item: Item)
   124     {
   125       item.heading_level match {
   126         case Some(i) =>
   127           close(_ > i)
   128           stack = (i + 1, item, buffer()) :: stack
   129         case None =>
   130       }
   131       stack.head._3 += Atom(item.source.length)
   132     }
   133   }
   134 
   135 
   136   /* outer syntax sections */
   137 
   138   private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item
   139   {
   140     override def name: String = command.span.name
   141     override def source: String = command.source
   142     override def heading_level: Option[Int] =
   143     {
   144       name match {
   145         case Thy_Header.CHAPTER => Some(0)
   146         case Thy_Header.SECTION => Some(1)
   147         case Thy_Header.SUBSECTION => Some(2)
   148         case Thy_Header.SUBSUBSECTION => Some(3)
   149         case Thy_Header.PARAGRAPH => Some(4)
   150         case Thy_Header.SUBPARAGRAPH => Some(5)
   151         case _ if is_theory_command(keywords, name) => Some(6)
   152         case _ => None
   153       }
   154     }
   155   }
   156 
   157   def parse_sections(
   158     syntax: Outer_Syntax,
   159     node_name: Document.Node.Name,
   160     text: CharSequence): List[Document] =
   161   {
   162     val sections = new Sections(syntax.keywords)
   163 
   164     for { span <- syntax.parse_spans(text) } {
   165       sections.add(
   166         new Command_Item(syntax.keywords,
   167           Command(Document_ID.none, node_name, Command.no_blobs, span)))
   168     }
   169     sections.result()
   170   }
   171 
   172 
   173   /* ML sections */
   174 
   175   private class ML_Item(token: ML_Lex.Token, level: Option[Int]) extends Item
   176   {
   177     override def source: String = token.source
   178     override def heading_level: Option[Int] = level
   179   }
   180 
   181   def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] =
   182   {
   183     val sections = new Sections(Keyword.Keywords.empty)
   184     val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None)
   185 
   186     var context: Scan.Line_Context = Scan.Finished
   187     for (line <- Library.separated_chunks(_ == '\n', text)) {
   188       val (toks, next_context) = ML_Lex.tokenize_line(SML, line, context)
   189       val level =
   190         toks.filterNot(_.is_space) match {
   191           case List(tok) if tok.is_comment =>
   192             val s = tok.source
   193             if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
   194             else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
   195             else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
   196             else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
   197             else None
   198           case _ => None
   199         }
   200       if (level.isDefined && context == Scan.Finished && next_context == Scan.Finished)
   201         toks.foreach(tok => sections.add(new ML_Item(tok, if (tok.is_comment) level else None)))
   202       else
   203         toks.foreach(tok => sections.add(new ML_Item(tok, None)))
   204 
   205       sections.add(nl)
   206       context = next_context
   207     }
   208     sections.result()
   209   }
   210 }