# HG changeset patch
# User wenzelm
# Date 1353360857 -3600
# Node ID 599c935aac828ad76a193e4e455397ebf5ea4457
# Parent  ff0b52a6d72f2247209eb8d50c3e4f8d7723f885
alternative completion for outer syntax keywords;

diff -r ff0b52a6d72f -r 599c935aac82 src/Doc/IsarRef/Spec.thy
--- 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
diff -r ff0b52a6d72f -r 599c935aac82 src/Pure/Isar/outer_syntax.scala
--- 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 =
diff -r ff0b52a6d72f -r 599c935aac82 src/Pure/PIDE/protocol.scala
--- 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) =>
       {
diff -r ff0b52a6d72f -r 599c935aac82 src/Pure/Pure.thy
--- 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"
diff -r ff0b52a6d72f -r 599c935aac82 src/Pure/Thy/thy_header.ML
--- 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 =
diff -r ff0b52a6d72f -r 599c935aac82 src/Pure/Thy/thy_header.scala
--- 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)])
 {