src/Pure/Thy/thy_header.scala
author wenzelm
Tue, 22 Dec 2009 21:48:17 +0100
changeset 34169 7501b2910900
parent 32466 a393b7e2a2f8
child 34188 fbfc18be1f8c
permissions -rw-r--r--
basic setup for header scanning/parsing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/thy_header.scala
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     3
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
     4
Theory headers -- independent of outer syntax.
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     5
*/
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     6
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     7
package isabelle
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     8
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     9
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    10
import scala.collection.mutable
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    11
import scala.util.parsing.input.{Reader, CharSequenceReader}
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    12
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    13
32466
a393b7e2a2f8 modernized Thy_Header;
wenzelm
parents: 32450
diff changeset
    14
object Thy_Header
32450
375db037f4d2 misc tuning;
wenzelm
parents: 29140
diff changeset
    15
{
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    16
  val HEADER = "header"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    17
  val THEORY = "theory"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    18
  val IMPORTS = "imports"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    19
  val USES = "uses"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    20
  val BEGIN = "begin"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    21
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    22
  val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    23
}
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    24
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    25
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    26
class Thy_Header(symbols: Symbol.Interpretation) extends Outer_Parse.Parser
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    27
{
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    28
  import Thy_Header._
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    29
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    30
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    31
  /* header */
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    32
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    33
  val header: Parser[(String, List[String], List[String])] =
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    34
  {
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    35
    val file_name = atom("file name", _.is_name)
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    36
    val theory_name = atom("theory name", _.is_name)
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    37
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    38
    val file =
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    39
      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    40
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    41
    val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    42
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    43
    val args =
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    44
      theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    45
        { case x ~ (_ ~ (ys ~ zs ~ _)) => (x, ys, zs) }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    46
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    47
    (keyword(HEADER) ~ tags) ~!
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    48
      ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    49
    (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    50
  }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    51
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    52
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    53
  /* scan -- lazy approximation */
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    54
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    55
  def scan(text: CharSequence): List[Outer_Lex.Token] =
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    56
  {
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    57
    val token = lexicon.token(symbols, _ => false)
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    58
    val toks = new mutable.ListBuffer[Outer_Lex.Token]
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    59
    def scan_until_begin(in: Reader[Char])
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    60
    {
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    61
      token(in) match {
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    62
        case lexicon.Success(tok, rest) =>
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    63
          toks += tok
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    64
          if (!(tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == BEGIN))
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    65
            scan_until_begin(rest)
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    66
        case _ =>
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    67
      }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    68
    }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    69
    scan_until_begin(new CharSequenceReader(text))
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    70
    toks.toList
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    71
  }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    72
}