src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 27353 71c4dd53d4cb
parent 27177 adefd3454174
child 27565 4bb03d4509e2
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -359,16 +359,15 @@
     1.4  (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
     1.5  
     1.6  fun lexicalstructure_keywords () =
     1.7 -    let val commands = OuterSyntax.dest_keywords ()
     1.8 -        fun category_of k = if k mem commands then "major" else "minor"
     1.9 -         (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
    1.10 -        fun keyword_elt (keyword,help,kind,_) =
    1.11 -            XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
    1.12 -                     [XML.Elem("shorthelp", [], [XML.Text help])])
    1.13 +    let val keywords = OuterKeyword.dest_keywords ()
    1.14 +        val commands = OuterKeyword.dest_commands ()
    1.15 +        fun keyword_elt kind keyword =
    1.16 +            XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
    1.17          in
    1.18              (* Also, note we don't call init_outer_syntax here to add interface commands,
    1.19              but they should never appear in scripts anyway so it shouldn't matter *)
    1.20 -            Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
    1.21 +            Lexicalstructure
    1.22 +              {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
    1.23          end
    1.24  
    1.25  (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;