| changeset 58900 | 1435cc20b022 |
| parent 58899 | 0a793c580685 |
| child 58903 | 38c72f5f6c2e |
| 58899:0a793c580685 | 58900:1435cc20b022 |
|---|---|
25 val IMPORTS = "imports" |
25 val IMPORTS = "imports" |
26 val KEYWORDS = "keywords" |
26 val KEYWORDS = "keywords" |
27 val AND = "and" |
27 val AND = "and" |
28 val BEGIN = "begin" |
28 val BEGIN = "begin" |
29 |
29 |
30 private val lexicon = |
30 private val keywords = |
31 Scan.Lexicon("%", "(", ")", ",", "::", "==", AND, BEGIN, |
31 Keyword.Keywords( |
32 HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY) |
32 List("%", "(", ")", ",", "::", "==", AND, BEGIN, |
33 HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY)) |
|
33 |
34 |
34 |
35 |
35 /* theory file name */ |
36 /* theory file name */ |
36 |
37 |
37 private val Base_Name = new Regex(""".*?([^/\\:]+)""") |
38 private val Base_Name = new Regex(""".*?([^/\\:]+)""") |
93 |
94 |
94 /* read -- lazy scanning */ |
95 /* read -- lazy scanning */ |
95 |
96 |
96 def read(reader: Reader[Char]): Thy_Header = |
97 def read(reader: Reader[Char]): Thy_Header = |
97 { |
98 { |
98 val token = Token.Parsers.token(lexicon, Scan.Lexicon.empty) |
99 val token = Token.Parsers.token(keywords) |
99 val toks = new mutable.ListBuffer[Token] |
100 val toks = new mutable.ListBuffer[Token] |
100 |
101 |
101 @tailrec def scan_to_begin(in: Reader[Char]) |
102 @tailrec def scan_to_begin(in: Reader[Char]) |
102 { |
103 { |
103 token(in) match { |
104 token(in) match { |
119 read(new CharSequenceReader(source)) |
120 read(new CharSequenceReader(source)) |
120 |
121 |
121 |
122 |
122 /* keywords */ |
123 /* keywords */ |
123 |
124 |
124 type Keywords = List[(String, Option[((String, List[String]), List[String])], Option[String])] |
125 type Keywords = List[(String, Option[Keyword.Spec], Option[String])] |
125 } |
126 } |
126 |
127 |
127 |
128 |
128 sealed case class Thy_Header( |
129 sealed case class Thy_Header( |
129 name: String, |
130 name: String, |