author | wenzelm |
Mon, 19 Nov 2012 22:34:17 +0100 | |
changeset 50128 | 599c935aac82 |
parent 48882 | 61dc7d5d150a |
child 51293 | 05b1bbae748d |
permissions | -rw-r--r-- |
28495 | 1 |
/* Title: Pure/Thy/thy_header.scala |
2 |
Author: Makarius |
|
3 |
||
46939 | 4 |
Static theory header information. |
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 |
|
48409 | 15 |
import java.io.{File => JFile} |
34188
fbfc18be1f8c
scan: operate on file (via Scan.byte_reader), more robust exception handling;
wenzelm
parents:
34169
diff
changeset
|
16 |
|
34169 | 17 |
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43652
diff
changeset
|
18 |
object Thy_Header extends Parse.Parser |
32450 | 19 |
{ |
28495 | 20 |
val HEADER = "header" |
21 |
val THEORY = "theory" |
|
22 |
val IMPORTS = "imports" |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
23 |
val KEYWORDS = "keywords" |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
24 |
val AND = "and" |
28495 | 25 |
val USES = "uses" |
26 |
val BEGIN = "begin" |
|
27 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
28 |
private val lexicon = |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
29 |
Scan.Lexicon("%", "(", ")", ",", "::", ";", "==", |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
30 |
AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES) |
34190 | 31 |
|
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
32 |
|
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
44159
diff
changeset
|
33 |
/* theory file name */ |
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
44159
diff
changeset
|
34 |
|
44225
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
35 |
private val Base_Name = new Regex(""".*?([^/\\:]+)""") |
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44185
diff
changeset
|
36 |
private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""") |
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
44159
diff
changeset
|
37 |
|
44225
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
38 |
def base_name(s: String): String = |
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
39 |
s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) } |
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
40 |
|
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44185
diff
changeset
|
41 |
def thy_name(s: String): Option[String] = |
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44185
diff
changeset
|
42 |
s match { case Thy_Name(name) => Some(name) case _ => None } |
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
43 |
|
34169 | 44 |
|
45 |
/* header */ |
|
46 |
||
44159 | 47 |
val header: Parser[Thy_Header] = |
34169 | 48 |
{ |
43611 | 49 |
val file_name = atom("file name", _.is_name) |
34169 | 50 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
51 |
val opt_files = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
52 |
keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } | |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
53 |
success(Nil) |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
54 |
val keyword_spec = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
55 |
atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^ |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
56 |
{ case x ~ y ~ z => ((x, y), z) } |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
57 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
58 |
val keyword_decl = |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
59 |
rep1(string) ~ |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
60 |
opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~ |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
61 |
opt(keyword("==") ~! name ^^ { case _ ~ x => x }) ^^ |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
62 |
{ case xs ~ y ~ z => xs.map((_, y, z)) } |
46939 | 63 |
val keyword_decls = |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
64 |
keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
46939 | 65 |
{ case xs ~ yss => (xs :: yss).flatten } |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
66 |
|
34169 | 67 |
val file = |
44185 | 68 |
keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | |
69 |
file_name ^^ (x => (x, true)) |
|
34169 | 70 |
|
71 |
val args = |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
72 |
theory_name ~ |
48638 | 73 |
(opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
46939 | 74 |
(opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
75 |
(opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
76 |
keyword(BEGIN) ^^ |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
77 |
{ case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) } |
34169 | 78 |
|
79 |
(keyword(HEADER) ~ tags) ~! |
|
80 |
((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } | |
|
81 |
(keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } |
|
82 |
} |
|
83 |
||
84 |
||
34190 | 85 |
/* read -- lazy scanning */ |
34169 | 86 |
|
44159 | 87 |
def read(reader: Reader[Char]): Thy_Header = |
34169 | 88 |
{ |
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43672
diff
changeset
|
89 |
val token = lexicon.token(_ => false) |
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
90 |
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
|
91 |
|
43611 | 92 |
@tailrec def scan_to_begin(in: Reader[Char]) |
34169 | 93 |
{ |
94 |
token(in) match { |
|
95 |
case lexicon.Success(tok, rest) => |
|
96 |
toks += tok |
|
43611 | 97 |
if (!tok.is_begin) scan_to_begin(rest) |
34169 | 98 |
case _ => |
99 |
} |
|
100 |
} |
|
43611 | 101 |
scan_to_begin(reader) |
34190 | 102 |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
103 |
parse(commit(header), Token.reader(toks.toList)) match { |
34190 | 104 |
case Success(result, _) => result |
105 |
case bad => error(bad.toString) |
|
106 |
} |
|
34169 | 107 |
} |
43611 | 108 |
|
44159 | 109 |
def read(source: CharSequence): Thy_Header = |
43646 | 110 |
read(new CharSequenceReader(source)) |
111 |
||
48706 | 112 |
|
113 |
/* keywords */ |
|
114 |
||
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
115 |
type Keywords = List[(String, Option[((String, List[String]), List[String])], Option[String])] |
34169 | 116 |
} |
44159 | 117 |
|
118 |
||
44185 | 119 |
sealed case class Thy_Header( |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
120 |
name: String, |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
121 |
imports: List[String], |
48706 | 122 |
keywords: Thy_Header.Keywords, |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
123 |
uses: List[(String, Boolean)]) |
44159 | 124 |
{ |
125 |
def map(f: String => String): Thy_Header = |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
126 |
Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2))) |
44159 | 127 |
} |
128 |