clarified modules;
authorwenzelm
Thu Aug 04 11:17:11 2016 +0200 (2016-08-04)
changeset 63604d8de4f8b95eb
parent 63603 9d9ea2c6bc38
child 63605 c7916060f55e
clarified modules;
src/Pure/Isar/document_structure.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/build-jars
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/document_structure.scala	Thu Aug 04 11:17:11 2016 +0200
     1.3 @@ -0,0 +1,90 @@
     1.4 +/*  Title:      Pure/Isar/document_structure.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Overall document structure.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import scala.collection.mutable
    1.14 +import scala.annotation.tailrec
    1.15 +
    1.16 +
    1.17 +object Document_Structure
    1.18 +{
    1.19 +  /** section headings etc. **/
    1.20 +
    1.21 +  sealed abstract class Document { def length: Int }
    1.22 +  case class Block(name: String, text: String, body: List[Document]) extends Document
    1.23 +  { val length: Int = (0 /: body)(_ + _.length) }
    1.24 +  case class Atom(command: Command) extends Document
    1.25 +  { def length: Int = command.length }
    1.26 +
    1.27 +  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
    1.28 +  {
    1.29 +    val name = command.span.name
    1.30 +    name match {
    1.31 +      case Thy_Header.CHAPTER => Some(0)
    1.32 +      case Thy_Header.SECTION => Some(1)
    1.33 +      case Thy_Header.SUBSECTION => Some(2)
    1.34 +      case Thy_Header.SUBSUBSECTION => Some(3)
    1.35 +      case Thy_Header.PARAGRAPH => Some(4)
    1.36 +      case Thy_Header.SUBPARAGRAPH => Some(5)
    1.37 +      case _ =>
    1.38 +        keywords.kinds.get(name) match {
    1.39 +          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
    1.40 +          case _ => None
    1.41 +        }
    1.42 +    }
    1.43 +  }
    1.44 +
    1.45 +  def parse_document(
    1.46 +    syntax: Outer_Syntax,
    1.47 +    node_name: Document.Node.Name,
    1.48 +    text: CharSequence): List[Document] =
    1.49 +  {
    1.50 +    /* stack operations */
    1.51 +
    1.52 +    def buffer(): mutable.ListBuffer[Document] =
    1.53 +      new mutable.ListBuffer[Document]
    1.54 +
    1.55 +    var stack: List[(Int, Command, mutable.ListBuffer[Document])] =
    1.56 +      List((0, Command.empty, buffer()))
    1.57 +
    1.58 +    @tailrec def close(level: Int => Boolean)
    1.59 +    {
    1.60 +      stack match {
    1.61 +        case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
    1.62 +          body2 += Block(command.span.name, command.source, body.toList)
    1.63 +          stack = stack.tail
    1.64 +          close(level)
    1.65 +        case _ =>
    1.66 +      }
    1.67 +    }
    1.68 +
    1.69 +    def result(): List[Document] =
    1.70 +    {
    1.71 +      close(_ => true)
    1.72 +      stack.head._3.toList
    1.73 +    }
    1.74 +
    1.75 +    def add(command: Command)
    1.76 +    {
    1.77 +      heading_level(syntax.keywords, command) match {
    1.78 +        case Some(i) =>
    1.79 +          close(_ > i)
    1.80 +          stack = (i + 1, command, buffer()) :: stack
    1.81 +        case None =>
    1.82 +      }
    1.83 +      stack.head._3 += Atom(command)
    1.84 +    }
    1.85 +
    1.86 +
    1.87 +    /* result structure */
    1.88 +
    1.89 +    val spans = syntax.parse_spans(text)
    1.90 +    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
    1.91 +    result()
    1.92 +  }
    1.93 +}
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Aug 04 10:55:51 2016 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Aug 04 11:17:11 2016 +0200
     2.3 @@ -8,7 +8,6 @@
     2.4  
     2.5  
     2.6  import scala.collection.mutable
     2.7 -import scala.annotation.tailrec
     2.8  
     2.9  
    2.10  object Outer_Syntax
    2.11 @@ -42,19 +41,6 @@
    2.12      result += '"'
    2.13      result.toString
    2.14    }
    2.15 -
    2.16 -
    2.17 -  /* overall document structure */
    2.18 -
    2.19 -  sealed abstract class Document { def length: Int }
    2.20 -  case class Document_Block(name: String, text: String, body: List[Document]) extends Document
    2.21 -  {
    2.22 -    val length: Int = (0 /: body)(_ + _.length)
    2.23 -  }
    2.24 -  case class Document_Atom(command: Command) extends Document
    2.25 -  {
    2.26 -    def length: Int = command.length
    2.27 -  }
    2.28  }
    2.29  
    2.30  final class Outer_Syntax private(
    2.31 @@ -188,72 +174,4 @@
    2.32  
    2.33    def parse_spans(input: CharSequence): List[Command_Span.Span] =
    2.34      parse_spans(Token.explode(keywords, input))
    2.35 -
    2.36 -
    2.37 -  /* overall document structure */
    2.38 -
    2.39 -  def heading_level(command: Command): Option[Int] =
    2.40 -  {
    2.41 -    val name = command.span.name
    2.42 -    name match {
    2.43 -      case Thy_Header.CHAPTER => Some(0)
    2.44 -      case Thy_Header.SECTION => Some(1)
    2.45 -      case Thy_Header.SUBSECTION => Some(2)
    2.46 -      case Thy_Header.SUBSUBSECTION => Some(3)
    2.47 -      case Thy_Header.PARAGRAPH => Some(4)
    2.48 -      case Thy_Header.SUBPARAGRAPH => Some(5)
    2.49 -      case _ =>
    2.50 -        keywords.kinds.get(name) match {
    2.51 -          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
    2.52 -          case _ => None
    2.53 -        }
    2.54 -    }
    2.55 -  }
    2.56 -
    2.57 -  def parse_document(node_name: Document.Node.Name, text: CharSequence):
    2.58 -    List[Outer_Syntax.Document] =
    2.59 -  {
    2.60 -    /* stack operations */
    2.61 -
    2.62 -    def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
    2.63 -      new mutable.ListBuffer[Outer_Syntax.Document]
    2.64 -
    2.65 -    var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
    2.66 -      List((0, Command.empty, buffer()))
    2.67 -
    2.68 -    @tailrec def close(level: Int => Boolean)
    2.69 -    {
    2.70 -      stack match {
    2.71 -        case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
    2.72 -          body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
    2.73 -          stack = stack.tail
    2.74 -          close(level)
    2.75 -        case _ =>
    2.76 -      }
    2.77 -    }
    2.78 -
    2.79 -    def result(): List[Outer_Syntax.Document] =
    2.80 -    {
    2.81 -      close(_ => true)
    2.82 -      stack.head._3.toList
    2.83 -    }
    2.84 -
    2.85 -    def add(command: Command)
    2.86 -    {
    2.87 -      heading_level(command) match {
    2.88 -        case Some(i) =>
    2.89 -          close(_ > i)
    2.90 -          stack = (i + 1, command, buffer()) :: stack
    2.91 -        case None =>
    2.92 -      }
    2.93 -      stack.head._3 += Outer_Syntax.Document_Atom(command)
    2.94 -    }
    2.95 -
    2.96 -
    2.97 -    /* result structure */
    2.98 -
    2.99 -    val spans = parse_spans(text)
   2.100 -    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
   2.101 -    result()
   2.102 -  }
   2.103  }
     3.1 --- a/src/Pure/build-jars	Thu Aug 04 10:55:51 2016 +0200
     3.2 +++ b/src/Pure/build-jars	Thu Aug 04 11:17:11 2016 +0200
     3.3 @@ -49,6 +49,7 @@
     3.4    General/url.scala
     3.5    General/word.scala
     3.6    General/xz_file.scala
     3.7 +  Isar/document_structure.scala
     3.8    Isar/keyword.scala
     3.9    Isar/line_structure.scala
    3.10    Isar/outer_syntax.scala
     4.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 04 10:55:51 2016 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 04 11:17:11 2016 +0200
     4.3 @@ -118,11 +118,11 @@
     4.4      def make_tree(
     4.5        parent: DefaultMutableTreeNode,
     4.6        offset: Text.Offset,
     4.7 -      documents: List[Outer_Syntax.Document])
     4.8 +      documents: List[Document_Structure.Document])
     4.9      {
    4.10        (offset /: documents) { case (i, document) =>
    4.11          document match {
    4.12 -          case Outer_Syntax.Document_Block(name, text, body) =>
    4.13 +          case Document_Structure.Block(name, text, body) =>
    4.14              val range = Text.Range(i, i + document.length)
    4.15              val node =
    4.16                new DefaultMutableTreeNode(
    4.17 @@ -137,7 +137,8 @@
    4.18  
    4.19      node_name(buffer) match {
    4.20        case Some(name) =>
    4.21 -        make_tree(data.root, 0, syntax.parse_document(name, JEdit_Lib.buffer_text(buffer)))
    4.22 +        make_tree(data.root, 0,
    4.23 +          Document_Structure.parse_document(syntax, name, JEdit_Lib.buffer_text(buffer)))
    4.24          true
    4.25        case None => false
    4.26      }