src/Pure/Interface/proof_general.ML
changeset 6947 a233bc746c75
parent 6861 7f9798c6ca8c
child 7027 ca0fbe679bbb
equal deleted inserted replaced
6946:309276732ee1 6947:a233bc746c75
     5 Configuration for ProofGeneral of LFCS Edinburgh.
     5 Configuration for ProofGeneral of LFCS Edinburgh.
     6 *)
     6 *)
     7 
     7 
     8 signature PROOF_GENERAL =
     8 signature PROOF_GENERAL =
     9 sig
     9 sig
    10   val write_keywords: string -> unit
    10   val write_keywords: unit -> unit
    11   val setup: (theory -> theory) list
    11   val setup: (theory -> theory) list
    12   val init: bool -> unit
    12   val init: bool -> unit
    13 end;
    13 end;
    14 
    14 
    15 structure ProofGeneral: PROOF_GENERAL =
    15 structure ProofGeneral: PROOF_GENERAL =
    39   \;;\n" ^
    39   \;;\n" ^
    40   defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^
    40   defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^
    41   implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
    41   implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
    42   "\n(provide 'isar-keywords)\n";
    42   "\n(provide 'isar-keywords)\n";
    43 
    43 
       
    44 val keywords_file = "isar-keywords.el";
       
    45 
    44 in
    46 in
    45 
    47 
    46 fun write_keywords file =
    48 fun write_keywords () =
    47   File.write (Path.unpack file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
    49   File.write (Path.unpack keywords_file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
    48 
    50 
    49 end;
    51 end;
    50 
    52 
    51 
    53 
    52 
    54