alternative completion for outer syntax keywords;
authorwenzelm
Mon Nov 19 22:34:17 2012 +0100 (2012-11-19 ago)
changeset 50128599c935aac82
parent 50127 ff0b52a6d72f
child 50129 e69db78b36d6
alternative completion for outer syntax keywords;
src/Doc/IsarRef/Spec.thy
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/protocol.scala
src/Pure/Pure.thy
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Doc/IsarRef/Spec.thy	Mon Nov 19 20:47:13 2012 +0100
     1.2 +++ b/src/Doc/IsarRef/Spec.thy	Mon Nov 19 22:34:17 2012 +0100
     1.3 @@ -55,7 +55,10 @@
     1.4      ;
     1.5      imports: @'imports' (@{syntax name} +)
     1.6      ;
     1.7 -    keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and')
     1.8 +    keywords: @'keywords' (keyword_decls + @'and')
     1.9 +    ;
    1.10 +    keyword_decls: (@{syntax string} +)
    1.11 +      ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
    1.12    "}
    1.13  
    1.14    \begin{description}
    1.15 @@ -81,6 +84,9 @@
    1.16    "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
    1.17    with and without proof, respectively.  Additional @{syntax tags}
    1.18    provide defaults for document preparation (\secref{sec:tags}).
    1.19 +
    1.20 +  It is possible to specify an alternative completion via @{text "==
    1.21 +  text"}, while the default is the corresponding keyword name.
    1.22    
    1.23    \item @{command (global) "end"} concludes the current theory
    1.24    definition.  Note that some other commands, e.g.\ local theory
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Nov 19 20:47:13 2012 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Nov 19 22:34:17 2012 +0100
     2.3 @@ -61,22 +61,29 @@
     2.4    def thy_load_commands: List[(String, List[String])] =
     2.5      (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
     2.6  
     2.7 -  def + (name: String, kind: (String, List[String]), replace: String): Outer_Syntax =
     2.8 +  def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
     2.9      new Outer_Syntax(
    2.10        keywords + (name -> kind),
    2.11        lexicon + name,
    2.12 -      if (Keyword.control(kind._1)) completion else completion + (name, replace))
    2.13 +      if (Keyword.control(kind._1) || replace == Some("")) completion
    2.14 +      else completion + (name, replace getOrElse name))
    2.15  
    2.16 -  def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, name)
    2.17 -  def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), name)
    2.18 -  def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    2.19 +  def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, Some(name))
    2.20 +  def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), Some(name))
    2.21 +  def + (name: String, replace: Option[String]): Outer_Syntax =
    2.22 +    this + (name, (Keyword.MINOR, Nil), replace)
    2.23 +  def + (name: String): Outer_Syntax = this + (name, None)
    2.24  
    2.25    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    2.26      (this /: keywords) {
    2.27 -      case (syntax, ((name, Some((kind, _))))) =>
    2.28 -        syntax + (Symbol.decode(name), kind) + (Symbol.encode(name), kind)
    2.29 -      case (syntax, ((name, None))) =>
    2.30 -        syntax + Symbol.decode(name) + Symbol.encode(name)
    2.31 +      case (syntax, ((name, Some((kind, _)), replace))) =>
    2.32 +        syntax +
    2.33 +          (Symbol.decode(name), kind, replace) +
    2.34 +          (Symbol.encode(name), kind, replace)
    2.35 +      case (syntax, ((name, None, replace))) =>
    2.36 +        syntax +
    2.37 +          (Symbol.decode(name), replace) +
    2.38 +          (Symbol.encode(name), replace)
    2.39      }
    2.40  
    2.41    def is_command(name: String): Boolean =
     3.1 --- a/src/Pure/PIDE/protocol.scala	Mon Nov 19 20:47:13 2012 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Nov 19 22:34:17 2012 +0100
     3.3 @@ -237,6 +237,7 @@
     3.4            { case Document.Node.Deps(header) =>
     3.5                val dir = Isabelle_System.posix_path(name.dir)
     3.6                val imports = header.imports.map(_.node)
     3.7 +              val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
     3.8                // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
     3.9                val uses = header.uses
    3.10                (Nil,
    3.11 @@ -244,7 +245,7 @@
    3.12                    pair(list(pair(Encode.string,
    3.13                      option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
    3.14                    pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
    3.15 -                (dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) },
    3.16 +                (dir, (name.theory, (imports, (keywords, (uses, header.errors))))))) },
    3.17            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
    3.18        def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    3.19        {
     4.1 --- a/src/Pure/Pure.thy	Mon Nov 19 20:47:13 2012 +0100
     4.2 +++ b/src/Pure/Pure.thy	Mon Nov 19 22:34:17 2012 +0100
     4.3 @@ -52,8 +52,10 @@
     4.4    and "theorem" "lemma" "corollary" :: thy_goal
     4.5    and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
     4.6    and "notepad" :: thy_decl
     4.7 -  and "have" "hence" :: prf_goal % "proof"
     4.8 -  and "show" "thus" :: prf_asm_goal % "proof"
     4.9 +  and "have" :: prf_goal % "proof"
    4.10 +  and "hence" :: prf_goal % "proof" == "then have"
    4.11 +  and "show" :: prf_asm_goal % "proof"
    4.12 +  and "thus" :: prf_asm_goal % "proof" == "then show"
    4.13    and "then" "from" "with" :: prf_chain % "proof"
    4.14    and "note" "using" "unfolding" :: prf_decl % "proof"
    4.15    and "fix" "assume" "presume" "def" :: prf_asm % "proof"
    4.16 @@ -66,7 +68,8 @@
    4.17    and "qed" :: qed_block % "proof"
    4.18    and "by" ".." "." "done" "sorry" :: "qed" % "proof"
    4.19    and "oops" :: qed_global % "proof"
    4.20 -  and "defer" "prefer" "apply" "apply_end" :: prf_script % "proof"
    4.21 +  and "defer" "prefer" "apply" :: prf_script % "proof"
    4.22 +  and "apply_end" :: prf_script % "proof" == ""
    4.23    and "proof" :: prf_block % "proof"
    4.24    and "also" "moreover" :: prf_decl % "proof"
    4.25    and "finally" "ultimately" :: prf_chain % "proof"
     5.1 --- a/src/Pure/Thy/thy_header.ML	Mon Nov 19 20:47:13 2012 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Nov 19 22:34:17 2012 +0100
     5.3 @@ -78,7 +78,7 @@
     5.4  
     5.5  val header_lexicons =
     5.6    pairself (Scan.make_lexicon o map Symbol.explode)
     5.7 -   (["%", "(", ")", ",", "::", ";", "and", beginN, importsN, keywordsN, usesN],
     5.8 +   (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN, usesN],
     5.9      [headerN, theoryN]);
    5.10  
    5.11  
    5.12 @@ -91,13 +91,20 @@
    5.13  
    5.14  val opt_files =
    5.15    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
    5.16 +
    5.17  val keyword_spec =
    5.18    Parse.group (fn () => "outer syntax keyword specification")
    5.19      (Parse.name -- opt_files -- Parse.tags);
    5.20  
    5.21 +val keyword_compl =
    5.22 +  Parse.group (fn () => "outer syntax keyword completion") Parse.name;
    5.23 +
    5.24  val keyword_decl =
    5.25 -  Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) >>
    5.26 -  (fn (names, spec) => map (rpair spec) names);
    5.27 +  Scan.repeat1 Parse.string --
    5.28 +  Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
    5.29 +  Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
    5.30 +  >> (fn ((names, spec), _) => map (rpair spec) names);
    5.31 +
    5.32  val keyword_decls = Parse.and_list1 keyword_decl >> flat;
    5.33  
    5.34  val file =
     6.1 --- a/src/Pure/Thy/thy_header.scala	Mon Nov 19 20:47:13 2012 +0100
     6.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Nov 19 22:34:17 2012 +0100
     6.3 @@ -26,7 +26,8 @@
     6.4    val BEGIN = "begin"
     6.5  
     6.6    private val lexicon =
     6.7 -    Scan.Lexicon("%", "(", ")", ",", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
     6.8 +    Scan.Lexicon("%", "(", ")", ",", "::", ";", "==",
     6.9 +      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
    6.10  
    6.11  
    6.12    /* theory file name */
    6.13 @@ -55,8 +56,10 @@
    6.14        { case x ~ y ~ z => ((x, y), z) }
    6.15  
    6.16      val keyword_decl =
    6.17 -      rep1(string) ~ opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
    6.18 -      { case xs ~ y => xs.map((_, y)) }
    6.19 +      rep1(string) ~
    6.20 +      opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    6.21 +      opt(keyword("==") ~! name ^^ { case _ ~ x => x }) ^^
    6.22 +      { case xs ~ y ~ z => xs.map((_, y, z)) }
    6.23      val keyword_decls =
    6.24        keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    6.25        { case xs ~ yss => (xs :: yss).flatten }
    6.26 @@ -109,12 +112,13 @@
    6.27  
    6.28    /* keywords */
    6.29  
    6.30 -  type Keywords = List[(String, Option[((String, List[String]), List[String])])]
    6.31 +  type Keywords = List[(String, Option[((String, List[String]), List[String])], Option[String])]
    6.32  }
    6.33  
    6.34  
    6.35  sealed case class Thy_Header(
    6.36 -  name: String, imports: List[String],
    6.37 +  name: String,
    6.38 +  imports: List[String],
    6.39    keywords: Thy_Header.Keywords,
    6.40    uses: List[(String, Boolean)])
    6.41  {