author | wenzelm |
Mon, 15 Feb 2016 14:55:44 +0100 | |
changeset 62337 | d3996d5873dd |
parent 61463 | 8e46cea6a45a |
child 62453 | b93cc7d73431 |
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 |
|
15 |
||
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43652
diff
changeset
|
16 |
object Thy_Header extends Parse.Parser |
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 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
20 |
type Keywords = List[(String, Option[Keyword.Spec], Option[String])] |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
21 |
|
61463 | 22 |
val HEADER = "header" /* FIXME legacy */ |
23 |
||
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
24 |
val CHAPTER = "chapter" |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
25 |
val SECTION = "section" |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
26 |
val SUBSECTION = "subsection" |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
27 |
val SUBSUBSECTION = "subsubsection" |
61463 | 28 |
val PARAGRAPH = "paragraph" |
29 |
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
|
30 |
val TEXT = "text" |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
31 |
val TXT = "txt" |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
32 |
val TEXT_RAW = "text_raw" |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
33 |
|
28495 | 34 |
val THEORY = "theory" |
35 |
val IMPORTS = "imports" |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
36 |
val KEYWORDS = "keywords" |
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 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
40 |
private val bootstrap_header: Keywords = |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
41 |
List( |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
42 |
("%", None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
43 |
("(", None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
44 |
(")", None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
45 |
(",", None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
46 |
("::", None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
47 |
("==", None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
48 |
(AND, None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
49 |
(BEGIN, None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
50 |
(IMPORTS, None, None), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
51 |
(KEYWORDS, None, None), |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
52 |
(HEADER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
53 |
(CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
54 |
(SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
55 |
(SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
56 |
(SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), |
61463 | 57 |
(PARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), |
58 |
(SUBPARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
59 |
(TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
60 |
(TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
61 |
(TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None), |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
62 |
(THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None), |
60957
574254152856
support for ML files with/without debugger information;
wenzelm
parents:
60215
diff
changeset
|
63 |
("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None), |
574254152856
support for ML files with/without debugger information;
wenzelm
parents:
60215
diff
changeset
|
64 |
("ML_file_debug", Some((Keyword.THY_LOAD, Nil), List("ML")), None), |
574254152856
support for ML files with/without debugger information;
wenzelm
parents:
60215
diff
changeset
|
65 |
("ML_file_no_debug", Some((Keyword.THY_LOAD, Nil), List("ML")), None)) |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
66 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
67 |
private val bootstrap_keywords = |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
68 |
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
|
69 |
|
59736
5c1a0069b9d3
tight span for theory header, which is relevant for error positions (including semantic completion);
wenzelm
parents:
59705
diff
changeset
|
70 |
lazy val bootstrap_syntax: Outer_Syntax = |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
71 |
Outer_Syntax.init().add_keywords(bootstrap_header) |
34190 | 72 |
|
38149
3c380380beac
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents:
36956
diff
changeset
|
73 |
|
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
44159
diff
changeset
|
74 |
/* 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
|
75 |
|
44225
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
|
44225
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
79 |
def base_name(s: String): String = |
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
80 |
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
|
81 |
|
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44185
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
|
34169 | 85 |
|
86 |
/* header */ |
|
87 |
||
44159 | 88 |
val header: Parser[Thy_Header] = |
34169 | 89 |
{ |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
90 |
val opt_files = |
58908 | 91 |
$$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
92 |
success(Nil) |
59694 | 93 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
94 |
val keyword_spec = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
95 |
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
|
96 |
{ case x ~ y ~ z => ((x, y), z) } |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48706
diff
changeset
|
97 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
98 |
val keyword_decl = |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
99 |
rep1(string) ~ |
58908 | 100 |
opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~ |
101 |
opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^ |
|
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48882
diff
changeset
|
102 |
{ case xs ~ y ~ z => xs.map((_, y, z)) } |
59694 | 103 |
|
46939 | 104 |
val keyword_decls = |
58908 | 105 |
keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
46939 | 106 |
{ case xs ~ yss => (xs :: yss).flatten } |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
107 |
|
34169 | 108 |
val args = |
59694 | 109 |
position(theory_name) ~ |
60215 | 110 |
(opt($$$(IMPORTS) ~! rep1(position(theory_xname))) ^^ |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
111 |
{ case None => Nil case Some(_ ~ xs) => xs }) ~ |
58908 | 112 |
(opt($$$(KEYWORDS) ~! keyword_decls) ^^ |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
113 |
{ case None => Nil case Some(_ ~ xs) => xs }) ~ |
58908 | 114 |
$$$(BEGIN) ^^ |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
115 |
{ case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } |
34169 | 116 |
|
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
117 |
val heading = |
58907 | 118 |
(command(HEADER) | |
119 |
command(CHAPTER) | |
|
120 |
command(SECTION) | |
|
121 |
command(SUBSECTION) | |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
122 |
command(SUBSUBSECTION) | |
61463 | 123 |
command(PARAGRAPH) | |
124 |
command(SUBPARAGRAPH) | |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
125 |
command(TEXT) | |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
126 |
command(TXT) | |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
127 |
command(TEXT_RAW)) ~ |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
128 |
tags ~! document_source |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset
|
129 |
|
58907 | 130 |
(rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } |
34169 | 131 |
} |
132 |
||
133 |
||
34190 | 134 |
/* read -- lazy scanning */ |
34169 | 135 |
|
59705 | 136 |
def read(reader: Reader[Char], start: Token.Pos): Thy_Header = |
34169 | 137 |
{ |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58908
diff
changeset
|
138 |
val token = Token.Parsers.token(bootstrap_keywords) |
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
139 |
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
|
140 |
|
43611 | 141 |
@tailrec def scan_to_begin(in: Reader[Char]) |
34169 | 142 |
{ |
143 |
token(in) match { |
|
55494 | 144 |
case Token.Parsers.Success(tok, rest) => |
34169 | 145 |
toks += tok |
43611 | 146 |
if (!tok.is_begin) scan_to_begin(rest) |
34169 | 147 |
case _ => |
148 |
} |
|
149 |
} |
|
43611 | 150 |
scan_to_begin(reader) |
34190 | 151 |
|
59705 | 152 |
parse(commit(header), Token.reader(toks.toList, start)) match { |
34190 | 153 |
case Success(result, _) => result |
154 |
case bad => error(bad.toString) |
|
155 |
} |
|
34169 | 156 |
} |
43611 | 157 |
|
59705 | 158 |
def read(source: CharSequence, start: Token.Pos): Thy_Header = |
159 |
read(new CharSequenceReader(source), start) |
|
34169 | 160 |
} |
44159 | 161 |
|
162 |
||
44185 | 163 |
sealed case class Thy_Header( |
59694 | 164 |
name: (String, Position.T), |
165 |
imports: List[(String, Position.T)], |
|
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
166 |
keywords: Thy_Header.Keywords) |
44159 | 167 |
{ |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
168 |
def decode_symbols: Thy_Header = |
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
169 |
{ |
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
170 |
val f = Symbol.decode _ |
59694 | 171 |
Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }), |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
172 |
keywords.map({ case (a, b, c) => |
58899 | 173 |
(f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) })) |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
174 |
} |
44159 | 175 |
} |