author | wenzelm |
Sun, 03 Jul 2011 19:42:32 +0200 | |
changeset 43648 | e32de528b5ef |
parent 43646 | 598b2c6ce13f |
child 43652 | dcd0b667f73d |
permissions | -rw-r--r-- |
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 |
||
43611 | 10 |
import scala.annotation.tailrec |
34169 | 11 |
import scala.collection.mutable |
43646 | 12 |
import scala.util.parsing.input.{Reader, CharSequenceReader} |
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
13 |
import scala.util.matching.Regex |
34169 | 14 |
|
34188
fbfc18be1f8c
scan: operate on file (via Scan.byte_reader), more robust exception handling;
wenzelm
parents:
34169
diff
changeset
|
15 |
import java.io.File |
fbfc18be1f8c
scan: operate on file (via Scan.byte_reader), more robust exception handling;
wenzelm
parents:
34169
diff
changeset
|
16 |
|
34169 | 17 |
|
32466 | 18 |
object Thy_Header |
32450 | 19 |
{ |
28495 | 20 |
val HEADER = "header" |
21 |
val THEORY = "theory" |
|
22 |
val IMPORTS = "imports" |
|
23 |
val USES = "uses" |
|
24 |
val BEGIN = "begin" |
|
25 |
||
34169 | 26 |
val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES) |
34190 | 27 |
|
34300 | 28 |
final case class Header(val name: String, val imports: List[String], val uses: List[String]) |
43611 | 29 |
{ |
30 |
def decode_permissive_utf8: Header = |
|
31 |
Header(Standard_System.decode_permissive_utf8(name), |
|
32 |
imports.map(Standard_System.decode_permissive_utf8), |
|
33 |
uses.map(Standard_System.decode_permissive_utf8)) |
|
34 |
} |
|
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
35 |
|
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
36 |
|
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
37 |
/* file name */ |
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
38 |
|
43648 | 39 |
def thy_path(name: String): Path = Path.basic(name).ext("thy") |
40 |
||
41 |
private val Thy_Path1 = new Regex("([^/]*)\\.thy") |
|
42 |
private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy") |
|
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
43 |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
38149
diff
changeset
|
44 |
def split_thy_path(path: String): Option[(String, String)] = |
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
45 |
path match { |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
38149
diff
changeset
|
46 |
case Thy_Path1(name) => Some(("", name)) |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
38149
diff
changeset
|
47 |
case Thy_Path2(dir, name) => Some((dir, name)) |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
38149
diff
changeset
|
48 |
case _ => None |
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
49 |
} |
28495 | 50 |
} |
34169 | 51 |
|
52 |
||
36948 | 53 |
class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser |
34169 | 54 |
{ |
55 |
import Thy_Header._ |
|
56 |
||
57 |
||
58 |
/* header */ |
|
59 |
||
34190 | 60 |
val header: Parser[Header] = |
34169 | 61 |
{ |
43611 | 62 |
val file_name = atom("file name", _.is_name) |
63 |
val theory_name = atom("theory name", _.is_name) |
|
34169 | 64 |
|
65 |
val file = |
|
66 |
keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name |
|
67 |
||
68 |
val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs } |
|
69 |
||
70 |
val args = |
|
71 |
theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^ |
|
34190 | 72 |
{ case x ~ (_ ~ (ys ~ zs ~ _)) => Header(x, ys, zs) } |
34169 | 73 |
|
74 |
(keyword(HEADER) ~ tags) ~! |
|
75 |
((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } | |
|
76 |
(keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } |
|
77 |
} |
|
78 |
||
79 |
||
34190 | 80 |
/* read -- lazy scanning */ |
34169 | 81 |
|
43611 | 82 |
def read(reader: Reader[Char]): Header = |
34169 | 83 |
{ |
84 |
val token = lexicon.token(symbols, _ => false) |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
85 |
val toks = new mutable.ListBuffer[Token] |
34188
fbfc18be1f8c
scan: operate on file (via Scan.byte_reader), more robust exception handling;
wenzelm
parents:
34169
diff
changeset
|
86 |
|
43611 | 87 |
@tailrec def scan_to_begin(in: Reader[Char]) |
34169 | 88 |
{ |
89 |
token(in) match { |
|
90 |
case lexicon.Success(tok, rest) => |
|
91 |
toks += tok |
|
43611 | 92 |
if (!tok.is_begin) scan_to_begin(rest) |
34169 | 93 |
case _ => |
94 |
} |
|
95 |
} |
|
43611 | 96 |
scan_to_begin(reader) |
34190 | 97 |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
98 |
parse(commit(header), Token.reader(toks.toList)) match { |
34190 | 99 |
case Success(result, _) => result |
100 |
case bad => error(bad.toString) |
|
101 |
} |
|
34169 | 102 |
} |
43611 | 103 |
|
43646 | 104 |
def read(source: CharSequence): Header = |
105 |
read(new CharSequenceReader(source)) |
|
106 |
||
43611 | 107 |
def read(file: File): Header = |
108 |
{ |
|
109 |
val reader = Scan.byte_reader(file) |
|
110 |
try { read(reader).decode_permissive_utf8 } |
|
111 |
finally { reader.close } |
|
112 |
} |
|
43648 | 113 |
|
114 |
||
115 |
/* check */ |
|
116 |
||
117 |
def check(name: String, source: CharSequence): Header = |
|
118 |
{ |
|
119 |
val header = read(source) |
|
120 |
val name1 = header.name |
|
121 |
if (name == name1) header |
|
122 |
else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1)) |
|
123 |
} |
|
34169 | 124 |
} |