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