tuned signature and modules;
authorwenzelm
Sun Oct 19 11:20:03 2014 +0200 (2014-10-19)
changeset 5870670a947611792
parent 58705 ad09a4635e26
child 58707 40abd7818bca
tuned signature and modules;
src/Pure/Isar/outer_syntax.scala
src/Pure/Thy/thy_structure.scala
src/Pure/build-jars
src/Tools/jEdit/src/isabelle_sidekick.scala
     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  }
     2.1 --- a/src/Pure/Thy/thy_structure.scala	Sat Oct 18 22:50:35 2014 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,71 +0,0 @@
     2.4 -/*  Title:      Pure/Thy/thy_structure.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Nested structure of theory source.
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -
    2.13 -import scala.collection.mutable
    2.14 -import scala.annotation.tailrec
    2.15 -
    2.16 -
    2.17 -object Thy_Structure
    2.18 -{
    2.19 -  sealed abstract class Entry { def length: Int }
    2.20 -  case class Block(val name: String, val body: List[Entry]) extends Entry
    2.21 -  {
    2.22 -    val length: Int = (0 /: body)(_ + _.length)
    2.23 -  }
    2.24 -  case class Atom(val command: Command) extends Entry
    2.25 -  {
    2.26 -    def length: Int = command.length
    2.27 -  }
    2.28 -
    2.29 -  def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
    2.30 -  {
    2.31 -    /* stack operations */
    2.32 -
    2.33 -    def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
    2.34 -    var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
    2.35 -      List((0, node_name.toString, buffer()))
    2.36 -
    2.37 -    @tailrec def close(level: Int => Boolean)
    2.38 -    {
    2.39 -      stack match {
    2.40 -        case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
    2.41 -          body2 += Block(name, body.toList)
    2.42 -          stack = stack.tail
    2.43 -          close(level)
    2.44 -        case _ =>
    2.45 -      }
    2.46 -    }
    2.47 -
    2.48 -    def result(): Entry =
    2.49 -    {
    2.50 -      close(_ => true)
    2.51 -      val (_, name, body) = stack.head
    2.52 -      Block(name, body.toList)
    2.53 -    }
    2.54 -
    2.55 -    def add(command: Command)
    2.56 -    {
    2.57 -      syntax.heading_level(command) match {
    2.58 -        case Some(i) =>
    2.59 -          close(_ > i)
    2.60 -          stack = (i + 1, command.source, buffer()) :: stack
    2.61 -        case None =>
    2.62 -      }
    2.63 -      stack.head._3 += Atom(command)
    2.64 -    }
    2.65 -
    2.66 -
    2.67 -    /* result structure */
    2.68 -
    2.69 -    val spans = syntax.parse_spans(text)
    2.70 -    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
    2.71 -    result()
    2.72 -  }
    2.73 -}
    2.74 -
     3.1 --- a/src/Pure/build-jars	Sat Oct 18 22:50:35 2014 +0200
     3.2 +++ b/src/Pure/build-jars	Sun Oct 19 11:20:03 2014 +0200
     3.3 @@ -83,7 +83,6 @@
     3.4    Thy/present.scala
     3.5    Thy/thy_header.scala
     3.6    Thy/thy_info.scala
     3.7 -  Thy/thy_structure.scala
     3.8    Thy/thy_syntax.scala
     3.9    Tools/bibtex.scala
    3.10    Tools/build.scala
     4.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Oct 18 22:50:35 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Oct 19 11:20:03 2014 +0200
     4.3 @@ -101,32 +101,34 @@
     4.4  {
     4.5    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
     4.6    {
     4.7 -    def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] =
     4.8 -      entry match {
     4.9 -        case Thy_Structure.Block(name, body) =>
    4.10 +    def make_tree(offset: Text.Offset, document: Outer_Syntax.Document)
    4.11 +        : List[DefaultMutableTreeNode] =
    4.12 +      document match {
    4.13 +        case Outer_Syntax.Document_Block(name, body) =>
    4.14            val node =
    4.15              new DefaultMutableTreeNode(
    4.16 -              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
    4.17 -          (offset /: body)((i, e) =>
    4.18 +              new Isabelle_Sidekick.Asset(
    4.19 +                Library.first_line(name), offset, offset + document.length))
    4.20 +          (offset /: body)((i, doc) =>
    4.21              {
    4.22 -              make_tree(i, e) foreach (nd => node.add(nd))
    4.23 -              i + e.length
    4.24 +              for (nd <- make_tree(i, doc)) node.add(nd)
    4.25 +              i + doc.length
    4.26              })
    4.27            List(node)
    4.28 -        case Thy_Structure.Atom(command)
    4.29 +
    4.30 +        case Outer_Syntax.Document_Atom(command)
    4.31          if command.is_proper && syntax.heading_level(command).isEmpty =>
    4.32            val node =
    4.33              new DefaultMutableTreeNode(
    4.34 -              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
    4.35 +              new Isabelle_Sidekick.Asset(command.name, offset, offset + document.length))
    4.36            List(node)
    4.37          case _ => Nil
    4.38        }
    4.39  
    4.40      node_name(buffer) match {
    4.41        case Some(name) =>
    4.42 -        val text = JEdit_Lib.buffer_text(buffer)
    4.43 -        val structure = Thy_Structure.parse(syntax, name, text)
    4.44 -        make_tree(0, structure) foreach (node => data.root.add(node))
    4.45 +        val document = syntax.parse_document(name, JEdit_Lib.buffer_text(buffer))
    4.46 +        for (node <- make_tree(0, document)) data.root.add(node)
    4.47          true
    4.48        case None => false
    4.49      }