author | haftmann |
Sun, 09 Feb 2020 22:03:07 +0000 | |
changeset 71426 | 745e518d3d0b |
parent 70713 | fd188463066e |
child 72747 | 5f9d66155081 |
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 |
64824 | 12 |
import scala.util.parsing.input.Reader |
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 |
|
15 |
||
68841 | 16 |
object Thy_Header |
32450 | 17 |
{ |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
18 |
/* bootstrap keywords */ |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
19 |
|
63579 | 20 |
type Keywords = List[(String, Keyword.Spec)] |
21 |
type Abbrevs = List[(String, String)] |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
22 |
|
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
23 |
val CHAPTER = "chapter" |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
24 |
val SECTION = "section" |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
25 |
val SUBSECTION = "subsection" |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
26 |
val SUBSUBSECTION = "subsubsection" |
61463 | 27 |
val PARAGRAPH = "paragraph" |
28 |
val SUBPARAGRAPH = "subparagraph" |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
29 |
val TEXT = "text" |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
30 |
val TXT = "txt" |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
31 |
val TEXT_RAW = "text_raw" |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
32 |
|
28495 | 33 |
val THEORY = "theory" |
34 |
val IMPORTS = "imports" |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
35 |
val KEYWORDS = "keywords" |
63579 | 36 |
val ABBREVS = "abbrevs" |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
37 |
val AND = "and" |
28495 | 38 |
val BEGIN = "begin" |
39 |
||
64854 | 40 |
val bootstrap_header: Keywords = |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
41 |
List( |
65384 | 42 |
("%", Keyword.Spec.none), |
43 |
("(", Keyword.Spec.none), |
|
44 |
(")", Keyword.Spec.none), |
|
45 |
(",", Keyword.Spec.none), |
|
46 |
("::", Keyword.Spec.none), |
|
47 |
("=", Keyword.Spec.none), |
|
48 |
(AND, Keyword.Spec.none), |
|
49 |
(BEGIN, Keyword.Spec(Keyword.QUASI_COMMAND)), |
|
50 |
(IMPORTS, Keyword.Spec(Keyword.QUASI_COMMAND)), |
|
51 |
(KEYWORDS, Keyword.Spec(Keyword.QUASI_COMMAND)), |
|
52 |
(ABBREVS, Keyword.Spec(Keyword.QUASI_COMMAND)), |
|
53 |
(CHAPTER, Keyword.Spec(Keyword.DOCUMENT_HEADING)), |
|
54 |
(SECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)), |
|
55 |
(SUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)), |
|
56 |
(SUBSUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)), |
|
57 |
(PARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)), |
|
58 |
(SUBPARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)), |
|
59 |
(TEXT, Keyword.Spec(Keyword.DOCUMENT_BODY)), |
|
60 |
(TXT, Keyword.Spec(Keyword.DOCUMENT_BODY)), |
|
61 |
(TEXT_RAW, Keyword.Spec(Keyword.DOCUMENT_RAW)), |
|
62 |
(THEORY, Keyword.Spec(Keyword.THY_BEGIN, tags = List("theory"))), |
|
63 |
("ML", Keyword.Spec(Keyword.THY_DECL, tags = List("ML")))) |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
64 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
65 |
private val bootstrap_keywords = |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
66 |
Keyword.Keywords.empty.add_keywords(bootstrap_header) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
67 |
|
67004
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
68 |
val bootstrap_syntax: Outer_Syntax = |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
69 |
Outer_Syntax.empty.add_keywords(bootstrap_header) |
34190 | 70 |
|
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
71 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64671
diff
changeset
|
72 |
/* file name vs. theory name */ |
62895
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
73 |
|
63022 | 74 |
val PURE = "Pure" |
62895
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
75 |
val ML_BOOTSTRAP = "ML_Bootstrap" |
65490 | 76 |
val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root") |
63022 | 77 |
val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a)) |
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
44159
diff
changeset
|
78 |
|
67215 | 79 |
val bootstrap_global_theories = |
80 |
(Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE) |
|
65490 | 81 |
|
65452 | 82 |
private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""") |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68841
diff
changeset
|
83 |
private val Split_File_Name = new Regex("""(.*?)[/\\]*([^/\\:]+)""") |
67212 | 84 |
private val File_Name = new Regex(""".*?([^/\\:]+)""") |
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
44159
diff
changeset
|
85 |
|
65526 | 86 |
def is_base_name(s: String): Boolean = |
87 |
s != "" && !s.exists("/\\:".contains(_)) |
|
88 |
||
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68841
diff
changeset
|
89 |
def split_file_name(s: String): Option[(String, String)] = |
67290 | 90 |
s match { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68841
diff
changeset
|
91 |
case Split_File_Name(s1, s2) => Some((s1, s2)) |
67290 | 92 |
case _ => None |
93 |
} |
|
94 |
||
65452 | 95 |
def import_name(s: String): String = |
67164 | 96 |
s match { |
67212 | 97 |
case File_Name(name) if !name.endsWith(".thy") => name |
67164 | 98 |
case _ => error("Malformed theory import: " + quote(s)) |
99 |
} |
|
44225
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
100 |
|
65452 | 101 |
def theory_name(s: String): String = |
62895
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
102 |
s match { |
66195 | 103 |
case Thy_File_Name(name) => bootstrap_name(name) |
67212 | 104 |
case File_Name(name) => |
67215 | 105 |
if (name == Sessions.root_name) name |
106 |
else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("") |
|
65452 | 107 |
case _ => "" |
62895
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
108 |
} |
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
109 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64671
diff
changeset
|
110 |
def is_ml_root(theory: String): Boolean = |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64671
diff
changeset
|
111 |
ml_roots.exists({ case (_, b) => b == theory }) |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64671
diff
changeset
|
112 |
|
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64671
diff
changeset
|
113 |
def is_bootstrap(theory: String): Boolean = |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64671
diff
changeset
|
114 |
bootstrap_thys.exists({ case (_, b) => b == theory }) |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64671
diff
changeset
|
115 |
|
66195 | 116 |
def bootstrap_name(theory: String): String = |
117 |
bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory) |
|
118 |
||
70713
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
119 |
def try_read_dir(dir: Path): List[String] = |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
120 |
{ |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
121 |
val files = |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
122 |
try { File.read_dir(dir) } |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
123 |
catch { case ERROR(_) => Nil } |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
124 |
for { Thy_File_Name(name) <- files } yield name |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
125 |
} |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
126 |
|
34169 | 127 |
|
68841 | 128 |
/* parser */ |
34169 | 129 |
|
68841 | 130 |
trait Parser extends Parse.Parser |
34169 | 131 |
{ |
68841 | 132 |
val header: Parser[Thy_Header] = |
133 |
{ |
|
134 |
val opt_files = |
|
135 |
$$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | |
|
136 |
success(Nil) |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
137 |
|
68841 | 138 |
val keyword_spec = |
139 |
atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^ |
|
140 |
{ case x ~ y ~ z => Keyword.Spec(x, y, z) } |
|
59694 | 141 |
|
68841 | 142 |
val keyword_decl = |
143 |
rep1(string) ~ |
|
144 |
opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^ |
|
145 |
{ case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) } |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
146 |
|
68841 | 147 |
val keyword_decls = |
148 |
keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
|
149 |
{ case xs ~ yss => (xs :: yss).flatten } |
|
150 |
||
151 |
val abbrevs = |
|
152 |
rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^ |
|
153 |
{ case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) } |
|
63579 | 154 |
|
68841 | 155 |
val args = |
156 |
position(theory_name) ~ |
|
157 |
(opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^ |
|
158 |
{ case None => Nil case Some(_ ~ xs) => xs }) ~ |
|
159 |
(opt($$$(KEYWORDS) ~! keyword_decls) ^^ |
|
160 |
{ case None => Nil case Some(_ ~ xs) => xs }) ~ |
|
161 |
(opt($$$(ABBREVS) ~! abbrevs) ^^ |
|
162 |
{ case None => Nil case Some(_ ~ xs) => xs }) ~ |
|
163 |
$$$(BEGIN) ^^ |
|
164 |
{ case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ => |
|
165 |
val f = Symbol.decode _ |
|
166 |
Thy_Header((f(name), pos), |
|
167 |
imports.map({ case (a, b) => (f(a), b) }), |
|
168 |
keywords.map({ case (a, Keyword.Spec(b, c, d)) => |
|
169 |
(f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }), |
|
170 |
abbrevs.map({ case (a, b) => (f(a), f(b)) })) |
|
171 |
} |
|
34169 | 172 |
|
68841 | 173 |
val heading = |
174 |
(command(CHAPTER) | |
|
175 |
command(SECTION) | |
|
176 |
command(SUBSECTION) | |
|
177 |
command(SUBSUBSECTION) | |
|
178 |
command(PARAGRAPH) | |
|
179 |
command(SUBPARAGRAPH) | |
|
180 |
command(TEXT) | |
|
181 |
command(TXT) | |
|
182 |
command(TEXT_RAW)) ~ |
|
69887 | 183 |
annotation ~! document_source |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
184 |
|
69887 | 185 |
(rep(heading) ~ command(THEORY) ~ annotation) ~! args ^^ { case _ ~ x => x } |
68841 | 186 |
} |
34169 | 187 |
} |
188 |
||
189 |
||
34190 | 190 |
/* read -- lazy scanning */ |
34169 | 191 |
|
65539 | 192 |
private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) = |
34169 | 193 |
{ |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
194 |
val token = Token.Parsers.token(bootstrap_keywords) |
64825 | 195 |
def make_tokens(in: Reader[Char]): Stream[Token] = |
34169 | 196 |
token(in) match { |
64825 | 197 |
case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest) |
198 |
case _ => Stream.empty |
|
34169 | 199 |
} |
64825 | 200 |
|
65539 | 201 |
val all_tokens = make_tokens(reader) |
202 |
val drop_tokens = |
|
203 |
if (strict) Nil |
|
204 |
else all_tokens.takeWhile(tok => !tok.is_command(Thy_Header.THEORY)).toList |
|
34190 | 205 |
|
65539 | 206 |
val tokens = all_tokens.drop(drop_tokens.length) |
64825 | 207 |
val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList |
208 |
val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList |
|
209 |
||
65539 | 210 |
(drop_tokens, tokens1 ::: tokens2) |
211 |
} |
|
212 |
||
68841 | 213 |
private object Parser extends Parser |
214 |
{ |
|
215 |
def parse_header(tokens: List[Token], pos: Token.Pos): Thy_Header = |
|
216 |
parse(commit(header), Token.reader(tokens, pos)) match { |
|
217 |
case Success(result, _) => result |
|
218 |
case bad => error(bad.toString) |
|
219 |
} |
|
220 |
} |
|
221 |
||
65539 | 222 |
def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header = |
223 |
{ |
|
224 |
val (_, tokens0) = read_tokens(reader, true) |
|
66918
ec2b50aeb0dd
more robust treatment of UTF8 in raw byte sources;
wenzelm
parents:
66713
diff
changeset
|
225 |
val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0)) |
65539 | 226 |
|
227 |
val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict) |
|
228 |
val pos = (start /: drop_tokens)(_.advance(_)) |
|
229 |
||
68841 | 230 |
Parser.parse_header(tokens, pos) |
34169 | 231 |
} |
232 |
} |
|
44159 | 233 |
|
44185 | 234 |
sealed case class Thy_Header( |
70638
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69887
diff
changeset
|
235 |
name_pos: (String, Position.T), |
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69887
diff
changeset
|
236 |
imports_pos: List[(String, Position.T)], |
63579 | 237 |
keywords: Thy_Header.Keywords, |
238 |
abbrevs: Thy_Header.Abbrevs) |
|
70638
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69887
diff
changeset
|
239 |
{ |
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69887
diff
changeset
|
240 |
def name: String = name_pos._1 |
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69887
diff
changeset
|
241 |
def pos: Position.T = name_pos._2 |
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69887
diff
changeset
|
242 |
def imports: List[String] = imports_pos.map(_._1) |
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69887
diff
changeset
|
243 |
} |