equal
deleted
inserted
replaced
13 import scala.util.matching.Regex |
13 import scala.util.matching.Regex |
14 |
14 |
15 import java.io.File |
15 import java.io.File |
16 |
16 |
17 |
17 |
18 object Thy_Header |
18 object Thy_Header extends Parse.Parser |
19 { |
19 { |
20 val HEADER = "header" |
20 val HEADER = "header" |
21 val THEORY = "theory" |
21 val THEORY = "theory" |
22 val IMPORTS = "imports" |
22 val IMPORTS = "imports" |
23 val USES = "uses" |
23 val USES = "uses" |
45 path match { |
45 path match { |
46 case Thy_Path1(name) => Some(("", name)) |
46 case Thy_Path1(name) => Some(("", name)) |
47 case Thy_Path2(dir, name) => Some((dir, name)) |
47 case Thy_Path2(dir, name) => Some((dir, name)) |
48 case _ => None |
48 case _ => None |
49 } |
49 } |
50 } |
|
51 |
|
52 |
|
53 class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser |
|
54 { |
|
55 import Thy_Header._ |
|
56 |
50 |
57 |
51 |
58 /* header */ |
52 /* header */ |
59 |
53 |
60 val header: Parser[Header] = |
54 val header: Parser[Header] = |
79 |
73 |
80 /* read -- lazy scanning */ |
74 /* read -- lazy scanning */ |
81 |
75 |
82 def read(reader: Reader[Char]): Header = |
76 def read(reader: Reader[Char]): Header = |
83 { |
77 { |
84 val token = lexicon.token(symbols, _ => false) |
78 val token = lexicon.token(Isabelle_System.symbols, _ => false) |
85 val toks = new mutable.ListBuffer[Token] |
79 val toks = new mutable.ListBuffer[Token] |
86 |
80 |
87 @tailrec def scan_to_begin(in: Reader[Char]) |
81 @tailrec def scan_to_begin(in: Reader[Char]) |
88 { |
82 { |
89 token(in) match { |
83 token(in) match { |
117 def check(name: String, source: CharSequence): Header = |
111 def check(name: String, source: CharSequence): Header = |
118 { |
112 { |
119 val header = read(source) |
113 val header = read(source) |
120 val name1 = header.name |
114 val name1 = header.name |
121 if (name == name1) header |
115 if (name == name1) header |
122 else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1)) |
116 else error("Bad file name " + thy_path(name) + " for theory " + quote(name1)) |
123 } |
117 } |
124 } |
118 } |