tuned signature: more uniform Keyword.spec;
authorwenzelm
Sun Jul 10 11:18:35 2016 +0200 (2016-07-10)
changeset 63429baedd4724f08
parent 63428 005b490f0ce2
child 63430 9c5fcd355a2d
tuned signature: more uniform Keyword.spec;
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Isar/keyword.ML	Fri Jul 08 22:22:51 2016 +0200
     1.2 +++ b/src/Pure/Isar/keyword.ML	Sun Jul 10 11:18:35 2016 +0200
     1.3 @@ -33,13 +33,14 @@
     1.4    val prf_script_goal: string
     1.5    val prf_script_asm_goal: string
     1.6    type spec = (string * string list) * string list
     1.7 +  val no_spec: spec
     1.8    type keywords
     1.9    val minor_keywords: keywords -> Scan.lexicon
    1.10    val major_keywords: keywords -> Scan.lexicon
    1.11    val no_command_keywords: keywords -> keywords
    1.12    val empty_keywords: keywords
    1.13    val merge_keywords: keywords * keywords -> keywords
    1.14 -  val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
    1.15 +  val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords
    1.16    val is_keyword: keywords -> string -> bool
    1.17    val is_command: keywords -> string -> bool
    1.18    val is_literal: keywords -> string -> bool
    1.19 @@ -116,6 +117,8 @@
    1.20  
    1.21  type spec = (string * string list) * string list;
    1.22  
    1.23 +val no_spec: spec = (("", []), []);
    1.24 +
    1.25  type entry =
    1.26   {pos: Position.T,
    1.27    id: serial,
    1.28 @@ -131,7 +134,6 @@
    1.29    else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
    1.30  
    1.31  
    1.32 -
    1.33  (** keyword tables **)
    1.34  
    1.35  (* type keywords *)
    1.36 @@ -168,18 +170,17 @@
    1.37      Symtab.merge (K true) (commands1, commands2));
    1.38  
    1.39  val add_keywords =
    1.40 -  fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) =>
    1.41 -    (case opt_spec of
    1.42 -      NONE =>
    1.43 -        let
    1.44 -          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
    1.45 -        in (minor', major, commands) end
    1.46 -    | SOME spec =>
    1.47 -        let
    1.48 -          val entry = check_spec pos spec;
    1.49 -          val major' = Scan.extend_lexicon (Symbol.explode name) major;
    1.50 -          val commands' = Symtab.update (name, entry) commands;
    1.51 -        in (minor, major', commands') end)));
    1.52 +  fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
    1.53 +    if kind = "" then
    1.54 +      let
    1.55 +        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
    1.56 +      in (minor', major, commands) end
    1.57 +    else
    1.58 +      let
    1.59 +        val entry = check_spec pos spec;
    1.60 +        val major' = Scan.extend_lexicon (Symbol.explode name) major;
    1.61 +        val commands' = Symtab.update (name, entry) commands;
    1.62 +      in (minor, major', commands') end));
    1.63  
    1.64  
    1.65  (* keyword status *)
     2.1 --- a/src/Pure/Isar/keyword.scala	Fri Jul 08 22:22:51 2016 +0200
     2.2 +++ b/src/Pure/Isar/keyword.scala	Sun Jul 10 11:18:35 2016 +0200
     2.3 @@ -88,6 +88,8 @@
     2.4  
     2.5    type Spec = ((String, List[String]), List[String])
     2.6  
     2.7 +  val no_spec: Spec = (("", Nil), Nil)
     2.8 +
     2.9    object Keywords
    2.10    {
    2.11      def empty: Keywords = new Keywords()
    2.12 @@ -130,21 +132,19 @@
    2.13  
    2.14      /* add keywords */
    2.15  
    2.16 -    def + (name: String): Keywords = new Keywords(minor + name, major, commands)
    2.17 -    def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
    2.18 -    def + (name: String, kind_tags: (String, List[String])): Keywords =
    2.19 -    {
    2.20 -      val major1 = major + name
    2.21 -      val commands1 = commands + (name -> kind_tags)
    2.22 -      new Keywords(minor, major1, commands1)
    2.23 -    }
    2.24 +    def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords =
    2.25 +      if (kind == "") new Keywords(minor + name, major, commands)
    2.26 +      else {
    2.27 +        val major1 = major + name
    2.28 +        val commands1 = commands + (name -> (kind, tags))
    2.29 +        new Keywords(minor, major1, commands1)
    2.30 +      }
    2.31  
    2.32      def add_keywords(header: Thy_Header.Keywords): Keywords =
    2.33        (this /: header) {
    2.34 -        case (keywords, (name, None, _)) =>
    2.35 -          keywords + Symbol.decode(name) + Symbol.encode(name)
    2.36 -        case (keywords, (name, Some((kind_tags, _)), _)) =>
    2.37 -          keywords + (Symbol.decode(name), kind_tags) + (Symbol.encode(name), kind_tags)
    2.38 +        case (keywords, (name, ((kind, tags), _), _)) =>
    2.39 +          if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
    2.40 +          else keywords + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
    2.41        }
    2.42  
    2.43  
     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Jul 08 22:22:51 2016 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Jul 10 11:18:35 2016 +0200
     3.3 @@ -85,16 +85,10 @@
     3.4  
     3.5    /* add keywords */
     3.6  
     3.7 -  def + (name: String): Outer_Syntax = this + (name, None, None)
     3.8 -  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
     3.9 -  def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
    3.10 +  def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None)
    3.11      : Outer_Syntax =
    3.12    {
    3.13 -    val keywords1 =
    3.14 -      opt_kind match {
    3.15 -        case None => keywords + name
    3.16 -        case Some(kind) => keywords + (name, kind)
    3.17 -      }
    3.18 +    val keywords1 = keywords + (name, kind, tags)
    3.19      val completion1 =
    3.20        if (replace == Some("")) completion
    3.21        else completion + (name, replace getOrElse name)
    3.22 @@ -103,11 +97,10 @@
    3.23  
    3.24    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    3.25      (this /: keywords) {
    3.26 -      case (syntax, (name, opt_spec, replace)) =>
    3.27 -        val opt_kind = opt_spec.map(_._1)
    3.28 +      case (syntax, (name, ((kind, tags), _), replace)) =>
    3.29          syntax +
    3.30 -          (Symbol.decode(name), opt_kind, replace) +
    3.31 -          (Symbol.encode(name), opt_kind, replace)
    3.32 +          (Symbol.decode(name), kind, tags, replace) +
    3.33 +          (Symbol.encode(name), kind, tags, replace)
    3.34      }
    3.35  
    3.36  
     4.1 --- a/src/Pure/PIDE/protocol.ML	Fri Jul 08 22:22:51 2016 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Sun Jul 10 11:18:35 2016 +0200
     4.3 @@ -72,7 +72,7 @@
     4.4                          val (master, (name, (imports, (keywords, errors)))) =
     4.5                            pair string (pair string (pair (list string)
     4.6                              (pair (list (pair string
     4.7 -                              (option (pair (pair string (list string)) (list string)))))
     4.8 +                              (pair (pair string (list string)) (list string))))
     4.9                                (list YXML.string_of_body)))) a;
    4.10                          val imports' = map (rpair Position.none) imports;
    4.11                          val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
     5.1 --- a/src/Pure/PIDE/protocol.scala	Fri Jul 08 22:22:51 2016 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Jul 10 11:18:35 2016 +0200
     5.3 @@ -378,7 +378,7 @@
     5.4                (Nil,
     5.5                  pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
     5.6                    pair(list(pair(Encode.string,
     5.7 -                    option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
     5.8 +                    pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
     5.9                    list(Encode.string)))))(
    5.10                  (master_dir, (theory, (imports, (keywords, header.errors)))))) },
    5.11            { case Document.Node.Perspective(a, b, c) =>
     6.1 --- a/src/Pure/Thy/thy_header.ML	Fri Jul 08 22:22:51 2016 +0200
     6.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Jul 10 11:18:35 2016 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  signature THY_HEADER =
     6.6  sig
     6.7 -  type keywords = ((string * Position.T) * Keyword.spec option) list
     6.8 +  type keywords = ((string * Position.T) * Keyword.spec) list
     6.9    type header =
    6.10     {name: string * Position.T,
    6.11      imports: (string * Position.T) list,
    6.12 @@ -32,7 +32,7 @@
    6.13  
    6.14  (* header *)
    6.15  
    6.16 -type keywords = ((string * Position.T) * Keyword.spec option) list;
    6.17 +type keywords = ((string * Position.T) * Keyword.spec) list;
    6.18  
    6.19  type header =
    6.20   {name: string * Position.T,
    6.21 @@ -63,27 +63,27 @@
    6.22  val bootstrap_keywords =
    6.23    Keyword.empty_keywords
    6.24    |> Keyword.add_keywords
    6.25 -    [(("%", @{here}), NONE),
    6.26 -     (("(", @{here}), NONE),
    6.27 -     ((")", @{here}), NONE),
    6.28 -     ((",", @{here}), NONE),
    6.29 -     (("::", @{here}), NONE),
    6.30 -     (("==", @{here}), NONE),
    6.31 -     (("and", @{here}), NONE),
    6.32 -     ((beginN, @{here}), NONE),
    6.33 -     ((importsN, @{here}), NONE),
    6.34 -     ((keywordsN, @{here}), NONE),
    6.35 -     ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
    6.36 -     ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    6.37 -     ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    6.38 -     ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    6.39 -     ((paragraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
    6.40 -     ((subparagraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
    6.41 -     ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
    6.42 -     ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
    6.43 -     ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
    6.44 -     ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
    6.45 -     (("ML", @{here}), SOME ((Keyword.thy_decl, []), ["ML"]))];
    6.46 +    [(("%", @{here}), Keyword.no_spec),
    6.47 +     (("(", @{here}), Keyword.no_spec),
    6.48 +     ((")", @{here}), Keyword.no_spec),
    6.49 +     ((",", @{here}), Keyword.no_spec),
    6.50 +     (("::", @{here}), Keyword.no_spec),
    6.51 +     (("==", @{here}), Keyword.no_spec),
    6.52 +     (("and", @{here}), Keyword.no_spec),
    6.53 +     ((beginN, @{here}), Keyword.no_spec),
    6.54 +     ((importsN, @{here}), Keyword.no_spec),
    6.55 +     ((keywordsN, @{here}), Keyword.no_spec),
    6.56 +     ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
    6.57 +     ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
    6.58 +     ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
    6.59 +     ((subsubsectionN, @{here}), ((Keyword.document_heading, []), [])),
    6.60 +     ((paragraphN, @{here}), ((Keyword.document_heading, []), [])),
    6.61 +     ((subparagraphN, @{here}), ((Keyword.document_heading, []), [])),
    6.62 +     ((textN, @{here}), ((Keyword.document_body, []), [])),
    6.63 +     ((txtN, @{here}), ((Keyword.document_body, []), [])),
    6.64 +     ((text_rawN, @{here}), ((Keyword.document_raw, []), [])),
    6.65 +     ((theoryN, @{here}), ((Keyword.thy_begin, []), ["theory"])),
    6.66 +     (("ML", @{here}), ((Keyword.thy_decl, []), ["ML"]))];
    6.67  
    6.68  
    6.69  (* theory data *)
    6.70 @@ -133,7 +133,7 @@
    6.71  
    6.72  val keyword_decl =
    6.73    Scan.repeat1 (Parse.position Parse.string) --
    6.74 -  Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
    6.75 +  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec --
    6.76    Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
    6.77    >> (fn ((names, spec), _) => map (rpair spec) names);
    6.78  
     7.1 --- a/src/Pure/Thy/thy_header.scala	Fri Jul 08 22:22:51 2016 +0200
     7.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 11:18:35 2016 +0200
     7.3 @@ -17,7 +17,7 @@
     7.4  {
     7.5    /* bootstrap keywords */
     7.6  
     7.7 -  type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
     7.8 +  type Keywords = List[(String, Keyword.Spec, Option[String])]
     7.9  
    7.10    val CHAPTER = "chapter"
    7.11    val SECTION = "section"
    7.12 @@ -37,27 +37,27 @@
    7.13  
    7.14    private val bootstrap_header: Keywords =
    7.15      List(
    7.16 -      ("%", None, None),
    7.17 -      ("(", None, None),
    7.18 -      (")", None, None),
    7.19 -      (",", None, None),
    7.20 -      ("::", None, None),
    7.21 -      ("==", None, None),
    7.22 -      (AND, None, None),
    7.23 -      (BEGIN, None, None),
    7.24 -      (IMPORTS, None, None),
    7.25 -      (KEYWORDS, None, None),
    7.26 -      (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.27 -      (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.28 -      (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.29 -      (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.30 -      (PARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.31 -      (SUBPARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.32 -      (TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    7.33 -      (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    7.34 -      (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
    7.35 -      (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
    7.36 -      ("ML", Some((Keyword.THY_DECL, Nil), List("ML")), None))
    7.37 +      ("%", Keyword.no_spec, None),
    7.38 +      ("(", Keyword.no_spec, None),
    7.39 +      (")", Keyword.no_spec, None),
    7.40 +      (",", Keyword.no_spec, None),
    7.41 +      ("::", Keyword.no_spec, None),
    7.42 +      ("==", Keyword.no_spec, None),
    7.43 +      (AND, Keyword.no_spec, None),
    7.44 +      (BEGIN, Keyword.no_spec, None),
    7.45 +      (IMPORTS, Keyword.no_spec, None),
    7.46 +      (KEYWORDS, Keyword.no_spec, None),
    7.47 +      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.48 +      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.49 +      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.50 +      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.51 +      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.52 +      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    7.53 +      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    7.54 +      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    7.55 +      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
    7.56 +      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory")), None),
    7.57 +      ("ML", ((Keyword.THY_DECL, Nil), List("ML")), None))
    7.58  
    7.59    private val bootstrap_keywords =
    7.60      Keyword.Keywords.empty.add_keywords(bootstrap_header)
    7.61 @@ -108,7 +108,7 @@
    7.62        rep1(string) ~
    7.63        opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    7.64        opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
    7.65 -      { case xs ~ y ~ z => xs.map((_, y, z)) }
    7.66 +      { case xs ~ y ~ z => xs.map((_, y.getOrElse(Keyword.no_spec), z)) }
    7.67  
    7.68      val keyword_decls =
    7.69        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    7.70 @@ -177,7 +177,7 @@
    7.71    {
    7.72      val f = Symbol.decode _
    7.73      Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
    7.74 -      keywords.map({ case (a, b, c) =>
    7.75 -        (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
    7.76 +      keywords.map({ case (a, ((x, y), z), c) =>
    7.77 +        (f(a), ((f(x), y.map(f)), z.map(f)), c.map(f)) }))
    7.78    }
    7.79  }
     8.1 --- a/src/Pure/Tools/find_consts.ML	Fri Jul 08 22:22:51 2016 +0200
     8.2 +++ b/src/Pure/Tools/find_consts.ML	Sun Jul 10 11:18:35 2016 +0200
     8.3 @@ -140,7 +140,8 @@
     8.4    Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
     8.5    Parse.typ >> Loose;
     8.6  
     8.7 -val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
     8.8 +val query_keywords =
     8.9 +  Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
    8.10  
    8.11  in
    8.12  
     9.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Jul 08 22:22:51 2016 +0200
     9.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Jul 10 11:18:35 2016 +0200
     9.3 @@ -521,7 +521,8 @@
     9.4    Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
     9.5    Parse.term >> Pattern;
     9.6  
     9.7 -val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
     9.8 +val query_keywords =
     9.9 +  Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
    9.10  
    9.11  in
    9.12