14 |
14 |
15 |
15 |
16 object Thy_Header extends Parse.Parser |
16 object Thy_Header extends Parse.Parser |
17 { |
17 { |
18 val HEADER = "header" |
18 val HEADER = "header" |
|
19 val CHAPTER = "chapter" |
|
20 val SECTION = "section" |
|
21 val SUBSECTION = "subsection" |
|
22 val SUBSUBSECTION = "subsubsection" |
|
23 |
19 val THEORY = "theory" |
24 val THEORY = "theory" |
20 val IMPORTS = "imports" |
25 val IMPORTS = "imports" |
21 val KEYWORDS = "keywords" |
26 val KEYWORDS = "keywords" |
22 val AND = "and" |
27 val AND = "and" |
23 val BEGIN = "begin" |
28 val BEGIN = "begin" |
24 |
29 |
25 private val lexicon = |
30 private val lexicon = |
26 Scan.Lexicon("%", "(", ")", ",", "::", "==", |
31 Scan.Lexicon("%", "(", ")", ",", "::", "==", AND, BEGIN, |
27 AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY) |
32 HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY) |
28 |
33 |
29 |
34 |
30 /* theory file name */ |
35 /* theory file name */ |
31 |
36 |
32 private val Base_Name = new Regex(""".*?([^/\\:]+)""") |
37 private val Base_Name = new Regex(""".*?([^/\\:]+)""") |
72 (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ |
77 (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ |
73 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
78 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
74 keyword(BEGIN) ^^ |
79 keyword(BEGIN) ^^ |
75 { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } |
80 { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } |
76 |
81 |
77 (keyword(HEADER) ~ tags) ~! |
82 val heading = |
78 ((document_source ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } | |
83 (keyword(HEADER) | |
79 (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } |
84 keyword(CHAPTER) | |
|
85 keyword(SECTION) | |
|
86 keyword(SUBSECTION) | |
|
87 keyword(SUBSUBSECTION)) ~ |
|
88 tags ~! document_source |
|
89 |
|
90 (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } |
80 } |
91 } |
81 |
92 |
82 |
93 |
83 /* read -- lazy scanning */ |
94 /* read -- lazy scanning */ |
84 |
95 |