--- a/src/Pure/Isar/keyword.ML Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/Isar/keyword.ML Sun Jul 10 11:18:35 2016 +0200
@@ -33,13 +33,14 @@
val prf_script_goal: string
val prf_script_asm_goal: string
type spec = (string * string list) * string list
+ val no_spec: spec
type keywords
val minor_keywords: keywords -> Scan.lexicon
val major_keywords: keywords -> Scan.lexicon
val no_command_keywords: keywords -> keywords
val empty_keywords: keywords
val merge_keywords: keywords * keywords -> keywords
- val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
+ val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords
val is_keyword: keywords -> string -> bool
val is_command: keywords -> string -> bool
val is_literal: keywords -> string -> bool
@@ -116,6 +117,8 @@
type spec = (string * string list) * string list;
+val no_spec: spec = (("", []), []);
+
type entry =
{pos: Position.T,
id: serial,
@@ -131,7 +134,6 @@
else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
-
(** keyword tables **)
(* type keywords *)
@@ -168,18 +170,17 @@
Symtab.merge (K true) (commands1, commands2));
val add_keywords =
- fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) =>
- (case opt_spec of
- NONE =>
- let
- val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
- in (minor', major, commands) end
- | SOME spec =>
- let
- val entry = check_spec pos spec;
- val major' = Scan.extend_lexicon (Symbol.explode name) major;
- val commands' = Symtab.update (name, entry) commands;
- in (minor, major', commands') end)));
+ fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
+ if kind = "" then
+ let
+ val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+ in (minor', major, commands) end
+ else
+ let
+ val entry = check_spec pos spec;
+ val major' = Scan.extend_lexicon (Symbol.explode name) major;
+ val commands' = Symtab.update (name, entry) commands;
+ in (minor, major', commands') end));
(* keyword status *)
--- a/src/Pure/Isar/keyword.scala Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/Isar/keyword.scala Sun Jul 10 11:18:35 2016 +0200
@@ -88,6 +88,8 @@
type Spec = ((String, List[String]), List[String])
+ val no_spec: Spec = (("", Nil), Nil)
+
object Keywords
{
def empty: Keywords = new Keywords()
@@ -130,21 +132,19 @@
/* add keywords */
- def + (name: String): Keywords = new Keywords(minor + name, major, commands)
- def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
- def + (name: String, kind_tags: (String, List[String])): Keywords =
- {
- val major1 = major + name
- val commands1 = commands + (name -> kind_tags)
- new Keywords(minor, major1, commands1)
- }
+ def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords =
+ if (kind == "") new Keywords(minor + name, major, commands)
+ else {
+ val major1 = major + name
+ val commands1 = commands + (name -> (kind, tags))
+ new Keywords(minor, major1, commands1)
+ }
def add_keywords(header: Thy_Header.Keywords): Keywords =
(this /: header) {
- case (keywords, (name, None, _)) =>
- keywords + Symbol.decode(name) + Symbol.encode(name)
- case (keywords, (name, Some((kind_tags, _)), _)) =>
- keywords + (Symbol.decode(name), kind_tags) + (Symbol.encode(name), kind_tags)
+ case (keywords, (name, ((kind, tags), _), _)) =>
+ if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
+ else keywords + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
}
--- a/src/Pure/Isar/outer_syntax.scala Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Sun Jul 10 11:18:35 2016 +0200
@@ -85,16 +85,10 @@
/* add keywords */
- def + (name: String): Outer_Syntax = this + (name, None, None)
- def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
- def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
+ def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None)
: Outer_Syntax =
{
- val keywords1 =
- opt_kind match {
- case None => keywords + name
- case Some(kind) => keywords + (name, kind)
- }
+ val keywords1 = keywords + (name, kind, tags)
val completion1 =
if (replace == Some("")) completion
else completion + (name, replace getOrElse name)
@@ -103,11 +97,10 @@
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
(this /: keywords) {
- case (syntax, (name, opt_spec, replace)) =>
- val opt_kind = opt_spec.map(_._1)
+ case (syntax, (name, ((kind, tags), _), replace)) =>
syntax +
- (Symbol.decode(name), opt_kind, replace) +
- (Symbol.encode(name), opt_kind, replace)
+ (Symbol.decode(name), kind, tags, replace) +
+ (Symbol.encode(name), kind, tags, replace)
}
--- a/src/Pure/PIDE/protocol.ML Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/PIDE/protocol.ML Sun Jul 10 11:18:35 2016 +0200
@@ -72,7 +72,7 @@
val (master, (name, (imports, (keywords, errors)))) =
pair string (pair string (pair (list string)
(pair (list (pair string
- (option (pair (pair string (list string)) (list string)))))
+ (pair (pair string (list string)) (list string))))
(list YXML.string_of_body)))) a;
val imports' = map (rpair Position.none) imports;
val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
--- a/src/Pure/PIDE/protocol.scala Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/PIDE/protocol.scala Sun Jul 10 11:18:35 2016 +0200
@@ -378,7 +378,7 @@
(Nil,
pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
pair(list(pair(Encode.string,
- option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
+ pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
list(Encode.string)))))(
(master_dir, (theory, (imports, (keywords, header.errors)))))) },
{ case Document.Node.Perspective(a, b, c) =>
--- a/src/Pure/Thy/thy_header.ML Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Sun Jul 10 11:18:35 2016 +0200
@@ -6,7 +6,7 @@
signature THY_HEADER =
sig
- type keywords = ((string * Position.T) * Keyword.spec option) list
+ type keywords = ((string * Position.T) * Keyword.spec) list
type header =
{name: string * Position.T,
imports: (string * Position.T) list,
@@ -32,7 +32,7 @@
(* header *)
-type keywords = ((string * Position.T) * Keyword.spec option) list;
+type keywords = ((string * Position.T) * Keyword.spec) list;
type header =
{name: string * Position.T,
@@ -63,27 +63,27 @@
val bootstrap_keywords =
Keyword.empty_keywords
|> Keyword.add_keywords
- [(("%", @{here}), NONE),
- (("(", @{here}), NONE),
- ((")", @{here}), NONE),
- ((",", @{here}), NONE),
- (("::", @{here}), NONE),
- (("==", @{here}), NONE),
- (("and", @{here}), NONE),
- ((beginN, @{here}), NONE),
- ((importsN, @{here}), NONE),
- ((keywordsN, @{here}), NONE),
- ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
- ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
- ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
- ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
- ((paragraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
- ((subparagraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
- ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
- ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
- ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
- ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
- (("ML", @{here}), SOME ((Keyword.thy_decl, []), ["ML"]))];
+ [(("%", @{here}), Keyword.no_spec),
+ (("(", @{here}), Keyword.no_spec),
+ ((")", @{here}), Keyword.no_spec),
+ ((",", @{here}), Keyword.no_spec),
+ (("::", @{here}), Keyword.no_spec),
+ (("==", @{here}), Keyword.no_spec),
+ (("and", @{here}), Keyword.no_spec),
+ ((beginN, @{here}), Keyword.no_spec),
+ ((importsN, @{here}), Keyword.no_spec),
+ ((keywordsN, @{here}), Keyword.no_spec),
+ ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
+ ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
+ ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
+ ((subsubsectionN, @{here}), ((Keyword.document_heading, []), [])),
+ ((paragraphN, @{here}), ((Keyword.document_heading, []), [])),
+ ((subparagraphN, @{here}), ((Keyword.document_heading, []), [])),
+ ((textN, @{here}), ((Keyword.document_body, []), [])),
+ ((txtN, @{here}), ((Keyword.document_body, []), [])),
+ ((text_rawN, @{here}), ((Keyword.document_raw, []), [])),
+ ((theoryN, @{here}), ((Keyword.thy_begin, []), ["theory"])),
+ (("ML", @{here}), ((Keyword.thy_decl, []), ["ML"]))];
(* theory data *)
@@ -133,7 +133,7 @@
val keyword_decl =
Scan.repeat1 (Parse.position Parse.string) --
- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
+ Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec --
Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
>> (fn ((names, spec), _) => map (rpair spec) names);
--- a/src/Pure/Thy/thy_header.scala Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala Sun Jul 10 11:18:35 2016 +0200
@@ -17,7 +17,7 @@
{
/* bootstrap keywords */
- type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
+ type Keywords = List[(String, Keyword.Spec, Option[String])]
val CHAPTER = "chapter"
val SECTION = "section"
@@ -37,27 +37,27 @@
private val bootstrap_header: Keywords =
List(
- ("%", None, None),
- ("(", None, None),
- (")", None, None),
- (",", None, None),
- ("::", None, None),
- ("==", None, None),
- (AND, None, None),
- (BEGIN, None, None),
- (IMPORTS, None, None),
- (KEYWORDS, None, None),
- (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (PARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (SUBPARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
- (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
- (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
- (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
- ("ML", Some((Keyword.THY_DECL, Nil), List("ML")), None))
+ ("%", Keyword.no_spec, None),
+ ("(", Keyword.no_spec, None),
+ (")", Keyword.no_spec, None),
+ (",", Keyword.no_spec, None),
+ ("::", Keyword.no_spec, None),
+ ("==", Keyword.no_spec, None),
+ (AND, Keyword.no_spec, None),
+ (BEGIN, Keyword.no_spec, None),
+ (IMPORTS, Keyword.no_spec, None),
+ (KEYWORDS, Keyword.no_spec, None),
+ (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+ (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+ (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+ (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+ (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+ (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+ (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
+ (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
+ (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
+ (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory")), None),
+ ("ML", ((Keyword.THY_DECL, Nil), List("ML")), None))
private val bootstrap_keywords =
Keyword.Keywords.empty.add_keywords(bootstrap_header)
@@ -108,7 +108,7 @@
rep1(string) ~
opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
- { case xs ~ y ~ z => xs.map((_, y, z)) }
+ { case xs ~ y ~ z => xs.map((_, y.getOrElse(Keyword.no_spec), z)) }
val keyword_decls =
keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
@@ -177,7 +177,7 @@
{
val f = Symbol.decode _
Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
- keywords.map({ case (a, b, c) =>
- (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
+ keywords.map({ case (a, ((x, y), z), c) =>
+ (f(a), ((f(x), y.map(f)), z.map(f)), c.map(f)) }))
}
}
--- a/src/Pure/Tools/find_consts.ML Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/Tools/find_consts.ML Sun Jul 10 11:18:35 2016 +0200
@@ -140,7 +140,8 @@
Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
Parse.typ >> Loose;
-val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
+val query_keywords =
+ Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
in
--- a/src/Pure/Tools/find_theorems.ML Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/Tools/find_theorems.ML Sun Jul 10 11:18:35 2016 +0200
@@ -521,7 +521,8 @@
Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
Parse.term >> Pattern;
-val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
+val query_keywords =
+ Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
in