src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 27353 71c4dd53d4cb
parent 27177 adefd3454174
child 27565 4bb03d4509e2
equal deleted inserted replaced
27352:8adeff7fd4bc 27353:71c4dd53d4cb
   357 end;
   357 end;
   358 
   358 
   359 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
   359 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
   360 
   360 
   361 fun lexicalstructure_keywords () =
   361 fun lexicalstructure_keywords () =
   362     let val commands = OuterSyntax.dest_keywords ()
   362     let val keywords = OuterKeyword.dest_keywords ()
   363         fun category_of k = if k mem commands then "major" else "minor"
   363         val commands = OuterKeyword.dest_commands ()
   364          (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
   364         fun keyword_elt kind keyword =
   365         fun keyword_elt (keyword,help,kind,_) =
   365             XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
   366             XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
       
   367                      [XML.Elem("shorthelp", [], [XML.Text help])])
       
   368         in
   366         in
   369             (* Also, note we don't call init_outer_syntax here to add interface commands,
   367             (* Also, note we don't call init_outer_syntax here to add interface commands,
   370             but they should never appear in scripts anyway so it shouldn't matter *)
   368             but they should never appear in scripts anyway so it shouldn't matter *)
   371             Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
   369             Lexicalstructure
       
   370               {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
   372         end
   371         end
   373 
   372 
   374 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
   373 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
   375    hooks needed in outer_syntax.ML to do that. *)
   374    hooks needed in outer_syntax.ML to do that. *)
   376 
   375