src/Pure/Interface/proof_general.ML
changeset 6720 353bd9b74b1f
parent 6699 1471f2bd74a0
child 6724 b5007e5e8a1b
equal deleted inserted replaced
6719:7c2dafc8e801 6720:353bd9b74b1f
     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 setup: (theory -> theory) list
    11   val setup: (theory -> theory) list
    11   val init: bool -> unit
    12   val init: bool -> unit
    12 end;
    13 end;
    13 
    14 
    14 structure ProofGeneral: PROOF_GENERAL =
    15 structure ProofGeneral: PROOF_GENERAL =
    15 struct
    16 struct
       
    17 
       
    18 
       
    19 (** generate keyword classification file **)
       
    20 
       
    21 local
       
    22 
       
    23 val regexp_meta = explode ".*+?[]^$";
       
    24 val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
       
    25 
       
    26 fun defconst name strs =
       
    27   "\n(defconst isar-keywords-" ^ name ^
       
    28   "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
       
    29 
       
    30 fun make_elisp_commands commands kind =
       
    31   defconst kind (mapfilter (fn (c, k) => if k = kind then Some c else None) commands);
       
    32 
       
    33 fun make_elisp_syntax (keywords, commands) =
       
    34   ";;\n\
       
    35   \;; Keyword classification tables for Isabelle/Isar.\n\
       
    36   \;; This file generated by Isabelle -- DO NOT EDIT!\n\
       
    37   \;;\n\
       
    38   \;; $Id$\n\
       
    39   \;;\n" ^
       
    40   defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^
       
    41   implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
       
    42   "\n(provide 'isar-keywords)\n";
       
    43 
       
    44 in
       
    45 
       
    46 fun write_keywords file =
       
    47   File.write (Path.unpack file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
       
    48 
       
    49 end;
       
    50 
    16 
    51 
    17 
    52 
    18 (** compile-time theory setup **)
    53 (** compile-time theory setup **)
    19 
    54 
    20 (* token translations *)
    55 (* token translations *)