--- a/src/Doc/IsarRef/Spec.thy Mon Nov 19 20:47:13 2012 +0100
+++ b/src/Doc/IsarRef/Spec.thy Mon Nov 19 22:34:17 2012 +0100
@@ -55,7 +55,10 @@
;
imports: @'imports' (@{syntax name} +)
;
- keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and')
+ keywords: @'keywords' (keyword_decls + @'and')
+ ;
+ keyword_decls: (@{syntax string} +)
+ ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
"}
\begin{description}
@@ -81,6 +84,9 @@
"\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
with and without proof, respectively. Additional @{syntax tags}
provide defaults for document preparation (\secref{sec:tags}).
+
+ It is possible to specify an alternative completion via @{text "==
+ text"}, while the default is the corresponding keyword name.
\item @{command (global) "end"} concludes the current theory
definition. Note that some other commands, e.g.\ local theory
--- a/src/Pure/Isar/outer_syntax.scala Mon Nov 19 20:47:13 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Mon Nov 19 22:34:17 2012 +0100
@@ -61,22 +61,29 @@
def thy_load_commands: List[(String, List[String])] =
(for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
- def + (name: String, kind: (String, List[String]), replace: String): Outer_Syntax =
+ def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
new Outer_Syntax(
keywords + (name -> kind),
lexicon + name,
- if (Keyword.control(kind._1)) completion else completion + (name, replace))
+ if (Keyword.control(kind._1) || replace == Some("")) completion
+ else completion + (name, replace getOrElse name))
- def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, name)
- def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), name)
- def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
+ def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, Some(name))
+ def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), Some(name))
+ def + (name: String, replace: Option[String]): Outer_Syntax =
+ this + (name, (Keyword.MINOR, Nil), replace)
+ def + (name: String): Outer_Syntax = this + (name, None)
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
(this /: keywords) {
- case (syntax, ((name, Some((kind, _))))) =>
- syntax + (Symbol.decode(name), kind) + (Symbol.encode(name), kind)
- case (syntax, ((name, None))) =>
- syntax + Symbol.decode(name) + Symbol.encode(name)
+ case (syntax, ((name, Some((kind, _)), replace))) =>
+ syntax +
+ (Symbol.decode(name), kind, replace) +
+ (Symbol.encode(name), kind, replace)
+ case (syntax, ((name, None, replace))) =>
+ syntax +
+ (Symbol.decode(name), replace) +
+ (Symbol.encode(name), replace)
}
def is_command(name: String): Boolean =
--- a/src/Pure/PIDE/protocol.scala Mon Nov 19 20:47:13 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Nov 19 22:34:17 2012 +0100
@@ -237,6 +237,7 @@
{ case Document.Node.Deps(header) =>
val dir = Isabelle_System.posix_path(name.dir)
val imports = header.imports.map(_.node)
+ val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
// FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
val uses = header.uses
(Nil,
@@ -244,7 +245,7 @@
pair(list(pair(Encode.string,
option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
- (dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) },
+ (dir, (name.theory, (imports, (keywords, (uses, header.errors))))))) },
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
{
--- a/src/Pure/Pure.thy Mon Nov 19 20:47:13 2012 +0100
+++ b/src/Pure/Pure.thy Mon Nov 19 22:34:17 2012 +0100
@@ -52,8 +52,10 @@
and "theorem" "lemma" "corollary" :: thy_goal
and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
and "notepad" :: thy_decl
- and "have" "hence" :: prf_goal % "proof"
- and "show" "thus" :: prf_asm_goal % "proof"
+ and "have" :: prf_goal % "proof"
+ and "hence" :: prf_goal % "proof" == "then have"
+ and "show" :: prf_asm_goal % "proof"
+ and "thus" :: prf_asm_goal % "proof" == "then show"
and "then" "from" "with" :: prf_chain % "proof"
and "note" "using" "unfolding" :: prf_decl % "proof"
and "fix" "assume" "presume" "def" :: prf_asm % "proof"
@@ -66,7 +68,8 @@
and "qed" :: qed_block % "proof"
and "by" ".." "." "done" "sorry" :: "qed" % "proof"
and "oops" :: qed_global % "proof"
- and "defer" "prefer" "apply" "apply_end" :: prf_script % "proof"
+ and "defer" "prefer" "apply" :: prf_script % "proof"
+ and "apply_end" :: prf_script % "proof" == ""
and "proof" :: prf_block % "proof"
and "also" "moreover" :: prf_decl % "proof"
and "finally" "ultimately" :: prf_chain % "proof"
--- a/src/Pure/Thy/thy_header.ML Mon Nov 19 20:47:13 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML Mon Nov 19 22:34:17 2012 +0100
@@ -78,7 +78,7 @@
val header_lexicons =
pairself (Scan.make_lexicon o map Symbol.explode)
- (["%", "(", ")", ",", "::", ";", "and", beginN, importsN, keywordsN, usesN],
+ (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN, usesN],
[headerN, theoryN]);
@@ -91,13 +91,20 @@
val opt_files =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
+
val keyword_spec =
Parse.group (fn () => "outer syntax keyword specification")
(Parse.name -- opt_files -- Parse.tags);
+val keyword_compl =
+ Parse.group (fn () => "outer syntax keyword completion") Parse.name;
+
val keyword_decl =
- Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) >>
- (fn (names, spec) => map (rpair spec) names);
+ Scan.repeat1 Parse.string --
+ Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
+ Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
+ >> (fn ((names, spec), _) => map (rpair spec) names);
+
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
val file =
--- a/src/Pure/Thy/thy_header.scala Mon Nov 19 20:47:13 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala Mon Nov 19 22:34:17 2012 +0100
@@ -26,7 +26,8 @@
val BEGIN = "begin"
private val lexicon =
- Scan.Lexicon("%", "(", ")", ",", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
+ Scan.Lexicon("%", "(", ")", ",", "::", ";", "==",
+ AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
/* theory file name */
@@ -55,8 +56,10 @@
{ case x ~ y ~ z => ((x, y), z) }
val keyword_decl =
- rep1(string) ~ opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
- { case xs ~ y => xs.map((_, y)) }
+ rep1(string) ~
+ opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
+ opt(keyword("==") ~! name ^^ { case _ ~ x => x }) ^^
+ { case xs ~ y ~ z => xs.map((_, y, z)) }
val keyword_decls =
keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
{ case xs ~ yss => (xs :: yss).flatten }
@@ -109,12 +112,13 @@
/* keywords */
- type Keywords = List[(String, Option[((String, List[String]), List[String])])]
+ type Keywords = List[(String, Option[((String, List[String]), List[String])], Option[String])]
}
sealed case class Thy_Header(
- name: String, imports: List[String],
+ name: String,
+ imports: List[String],
keywords: Thy_Header.Keywords,
uses: List[(String, Boolean)])
{